The Coq mailing list

[Michel Levy <Michel.Levy AT imag.fr>]

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 :

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

Now it's impossible to Unfold f.
Coq < Goal (b:bool)((f b) = b).
1 subgoal
  
  ============================
   (b:bool)(f b)=b
Unnamed_thm < Intros.
1 subgoal
  
  b : bool
  ============================
   (f b)=b

Unnamed_thm < Unfold f.
Error: f does not denote an evaluable constant



-- 
Michel Levy  
Laboratoire L.S.R., Bureau C214, B.P.72 - 38042 SAINT MARTIN D'HERES
CEDEX 
e.mail : 
Michel.Levy AT imag.fr
    tel :(33)476514022
http://www-lsr.imag.fr/users/Michel.Levy