The Coq mailing list

[Xavier RIVAL <rival AT clipper.ens.fr>]

        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