coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Frédéric Blanqui <frederic.blanqui AT inria.fr>
- To: coq-club AT inria.fr
- Subject: Re: [Coq-Club] about 'function' definition clause
- Date: Tue, 10 Feb 2015 18:27:23 +0100
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.
- [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.