The Coq mailing list

[Hermann Lehner <hermann.lehner AT inf.ethz.ch>]

Hello all,

Some time ago (Mon, 30 Jul 2007 18:07:18 +0200), J.-F. Dufourd came 
across the following issue.

---snip----

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.
Proof. intros. omega. Defined.

is refused with the message:

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

---snip----

Anyone having an answer on that, as I have the same problem with a much 
larger definition. The little example above still does not work with Coq 
8.1pl3.

Does someone know which part of the function definition triggers this 
anomaly, so that it can be bypassed?

Thanks!

Best regards
  Hermann Lehner



--
http://www.hermann-lehner.com