The Coq mailing list

[Lionel Elie Mamane <lionel AT mamane.lu>]

Hi,

On Wed, Nov 27, 2002 at 01:21:48PM +0100, Benjamin Werner wrote:

>> I'm trying to define a function of the following shape

>> f (Tcons a) (Tcons b) = g (f a (Tcons b)) (f (Tcons a) b)

> Your function seems to have a form similar to Ackermann's function.
> all you have to do is use two embeded fixpoints.

Yes, works fine. Thanks. I could swear I had tried this (I had found
the example of the Ackermann function in the archives), but
failed. Somehow looking at it again made it work :-)

What's bugging me is that in my case, the lemma's "the function
satisfies to the (simple) equation defining it" are not "Trivial", but
maybe I just did a typing error that will spring in my face on
Monday, that makes those lemma's false for now.

-- 
Lionel

Attachment: pgpFNuBD0QNxo.pgp
Description: PGP signature