The Coq mailing list

[Laurent Thery <Laurent.Thery AT inria.fr>]

On 04/25/2017 08:55 AM, Pierre Casteran wrote:
> Hi,
>
>    I wrote a small proof on fast growing functions (Wainer's hierarchy).
>
>    The statement is F_3 (2) > F_omega (2). The proof term is not so big, 
> but it contains several occurrences of (f_2 23), which is known as 
> greater than 2^23.
>
>    The problem may come from the fact that all these subterms are 
> computed after Qed, thus I had to interrupt after some time. Is there an 
> option for preventing Coq to expand function calls ?

It should not expand it if not needed.
Can you abstract away f_2 23 by a f with some axioms to check if it is 
the culprit.

--
Laurent