coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Re: Stuck on termination proof (ha ha)

From: frank maltman <frank.maltman AT googlemail.com>
To: <coq-club AT inria.fr>
Subject: [Coq-Club] Re: Stuck on termination proof (ha ha)
Date: Sun, 31 Jul 2011 16:03:55 +0000

I've just noticed that function contained an error, but it doesn't
affect the question (as far as I know).

On Sun, 31 Jul 2011 15:11:11 +0000
frank maltman
<frank.maltman AT googlemail.com>
wrote:
>   | Term_Cond tc t0 t1 =>
>     match one_step t0 with

Should obviously read:

  | Term_Cond tc t0 t1 =>
    match one_step tc with

[Coq-Club] Stuck on termination proof (ha ha), frank maltman
- [Coq-Club] Re: Stuck on termination proof (ha ha), frank maltman