coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Continuity of coinductive definitions

From: Adam Chlipala <adamc AT cs.berkeley.edu>
To: Andrej.Bauer AT andrej.com
Cc: Coq Mailing List <coq-club AT pauillac.inria.fr>
Subject: Re: [Coq-Club] Continuity of coinductive definitions
Date: Mon, 18 Feb 2008 09:29:01 -0500
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Andrej Bauer wrote:

CoInductive halts : sigma -> Prop :=
| isFinished : halts Finished
| isNotYet : forall x : sigma, halts x -> halts (NotYet x).

Why make this type family co-inductive instead of inductive? Do you really want to be able to have infinite [halts] proofs that "cheat" and don't really prove halting?

[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