coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pascal Manoury <pascal.manoury AT pps.univ-paris-diderot.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] about 'function' definition clause
- Date: Tue, 10 Feb 2015 18:46:26 +0100
> 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.
>>
>
- [Coq-Club] about 'function' definition clause, Pascal Manoury, 02/10/2015
- Re: [Coq-Club] about 'function' definition clause, Frédéric Blanqui, 02/10/2015
- Re: [Coq-Club] about 'function' definition clause, Pascal Manoury, 02/10/2015
- Re: [Coq-Club] about 'function' definition clause, Matthieu Sozeau, 02/10/2015
- Re: [Coq-Club] about 'function' definition clause, Pascal Manoury, 02/10/2015
- Re: [Coq-Club] about 'function' definition clause, Frédéric Blanqui, 02/10/2015
Archive powered by MHonArc 2.6.18.