The Coq mailing list

[Eduardo Gimenez <Eduardo.Gimenez AT trusted-logic.fr>]

HI,

Just an extra precision about Xavier's remark: in V6.3.1, the command Save 
used to save the proof as a transparent object, while Qed saved it as an 
opaque one. This seems no longer to be the case in the new V7.1. 

Best,
Eduardo Gimenez.

Le Monday 08 October 2001 21:11, vous avez ?rit :
> Hi,
>
> On Mon, 8 Oct 2001, Michel Levy wrote:
> > Could you explain me what is an evaluable constant, more exactly, why I
> > can "Unfold h" directly defined by
> > Definition h :=  [H:bool]H  : bool->bool
> >
> > and why it's impossible when I defined f with a proof.
> > I give a short sequence leading to this situation :
>
>       Terms built in proof mode are "opaque" (i.e. non unfoldable)
> whereas terms defined directly are "tranparent" (i.e. unfoldable).
>       You can make a term t transparent by the "Transparent t." command.
> The converse is done by "Opaque t.".
>
>       For instance :
> > Coq < Definition f : bool -> bool.
> > 1 subgoal
> >
> >   ============================
> >    bool->bool
> >
> > f < Intro H; Assumption.
> > Subtree proved!
> >
> > f < Save.
> > Intro H; Assumption.
> >
> > f is defined
> >
> > Coq < Print f.
> > f = [H:bool]H
> >
> >      : bool->bool
>
> Coq < Transparent f.
>
> Coq < Goal (b:bool)((f b) = b).
> 1 subgoal
>
>   ============================
>    (b:bool)(f b)=b
>
> Unnamed_thm < Reflexivity.
> Subtree proved!
>
>
>       Xavier RIVAL