The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT lri.fr>]

On Wed, 12 Jul 2000, David Delahaye wrote:

>     Here is a trick to deal with your example:

This works indeed but you changed his definition. You can do the same
thing by using a usual Fixpoint definition.

I just want to remark that these kinds of problems arise since there is
no lexicographic comparaison in Coq. To solve this problem, we are obliged
to change the way we want to define the function, and it is not always
easy (ex. Ackermann function).

Frederic Blanqui.

------------------------------------------------------------------------------
Laboratoire de Recherche en Informatique (LRI) - Equipe DEMONS
batiment 490, bureau 153, Universite Paris-Sud 91405 ORSAY (FRANCE)
tel:01 69 15 42 35 - fax:01 69 15 65 86 - web:http://www.lri.fr/~blanqui