coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Continuity of coinductive definitions

From: Andrej Bauer <Andrej.Bauer AT fmf.uni-lj.si>
To: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Continuity of coinductive definitions
Date: Mon, 18 Feb 2008 21:30:50 +0100
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Edsko de Vries wrote:
> Inductive halts : sigma -> Prop :=
> | isFinished : halts Finished
> | isNotYet : forall x : sigma, halts x -> halts (NotYet x).

Argh! Yes of course, it should say "Inductive". With "CoInductive" we
can prove that everything halts (as was pointed out by Adam).

Thank you for correcting my "trivial" error.

Best regards,

Andrej

[Coq-Club] Continuity of coinductive definitions, Andrej Bauer
- Re: [Coq-Club] Continuity of coinductive definitions, Adam Chlipala
- Re: [Coq-Club] Continuity of coinductive definitions, Edsko de Vries
  - Re: [Coq-Club] Continuity of coinductive definitions, Pierre Casteran
  - Re: [Coq-Club] Continuity of coinductive definitions, Andrej Bauer