The Coq mailing list

[Vladimir Komendantsky <Vladimir.Komendantsky AT sophia.inria.fr>]

Well, I tried to run the snippet below in the svn version of Coq and 
everything went fine. There was no anomaly.
--
Vladimir


Hermann Lehner wrote:

> 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