Skip to Content.
Sympa Menu

coq-club - [Coq-Club] strange behavior of "Eval compute"

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] strange behavior of "Eval compute"


chronological Thread 
  • From: Vladimir Voevodsky <vladimir AT ias.edu>
  • To: Coq Club <coq-club AT inria.fr>
  • Subject: [Coq-Club] strange behavior of "Eval compute"
  • Date: Thu, 28 Oct 2010 14:26:19 -0400

Hello,

I am using "Eval compute in ..." to compute a term of type nat which is 
defined in a complicated way but should reduce to (S O).  When all the 
intermediate definitions are made transparent the computation goes through 
but when I make one definition opaque by ending it with Qed. instead of 
Defined.  the "Eval compute" hangs. 

Isn't it supposed to terminate anyway with whatever expression in a normal 
form it ends up with without unfolding the opaque definition?

Vladimir.






Archive powered by MhonArc 2.6.16.

Top of Page