The Coq mailing list

[Jean-Francois Dufourd <dufourd AT dpt-info.u-strasbg.fr>]

Hello all,

I'm trying to use the experimental Function features,
and I wonder that the following (extended) Euclidean division definition:

Function div(a b:nat){measure (fun m:nat=>m) a}:nat:=
 if eq_nat_dec b 0 then 0
 else if (le_lt_dec b a) then (div (a-b) b) + 1 else 0. 

the terminaison of which is proved by:

Proof. intros. omega. Defined.

is refused with the message:

"Anomaly: Cannot create equation Lemma. Please report".

What is wrong ? Thanks.

Best regards,

J.-F. Dufourd