coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] inductive definition and parameterised definition

From: Fr�d�ric Besson <fbesson AT irisa.fr>
To: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] inductive definition and parameterised definition
Date: Wed, 19 Sep 2007 15:54:51 +0200
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

On 19 sept. 07, at 15:05, Keiko Nakata wrote:

Definition good (p:Prop) := True /\ p.

Yet, I prefer to keep good opaque,�

instead provide an axiom for unfolding:

Parameter good: Prop -> Prop.

Axiom good_unfold: forall (p:Prop), good p = True /\ p.�

Hello,

You can make good opaque later on : Opaque good.

BTW, good_unfold is wrongly bracketed. you should have written:

� Lemma good_unfold: forall (p:Prop), good p = (True /\ p).

Fr�d�ric

[Coq-Club] inductive definition and parameterised definition, Keiko Nakata
- Re: [Coq-Club] inductive definition and parameterised definition, Fr�d�ric Besson