The Coq mailing list

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

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.