Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] about 'function' definition clause

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] about 'function' definition clause


Chronological Thread 
  • 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.





Archive powered by MHonArc 2.6.18.

Top of Page