The Coq mailing list

[Frédéric Blanqui <frederic.blanqui AT inria.fr>]

Hello. Why not taking a pair as argument, ordered lexicographically? 
Frédéric.

Le 10/02/2015 18:25, Pascal Manoury a écrit :
> Hello dear coqists,
>
>   I am trying with students to experiment the use of the 'function' 
> definition clause and ordinal measure for proving
> termination of recursive functions.
>
>   Unfortunately, we are stuck with the example of Ackermann's function 
> because the 'function' clause does not
> allow nested recursion.
>
>   Is there any way to relax this restriction, for instance, by generalizing 
> the nested recursive call when generating
> the proof obligation ?
>
>         Pascal Manoury.