The Coq mailing list

[Pascal Manoury <pascal.manoury AT pps.univ-paris-diderot.fr>]

> Hello. Why not taking a pair as argument, ordered lexicographically? 
> Frédéric.
 Because I am interested in using ordinal measure, not in proving Ackermann's 
termination :)

 We already use a pair as argument and the nested recursion in refused.

        Pascal Manoury.

> 
> 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.
>> 
>