The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

Hi Pascal,

  the Program extension might handle this better (i.e. allow nested 
recursion).
-- Matthieu

2015-02-10 18:27 GMT+01:00 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.
>>
>

-- Matthieu