coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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.
- [Coq-Club] strange behavior of "Eval compute", Vladimir Voevodsky
- RE: [Coq-Club] strange behavior of "Eval compute", Georges Gonthier
Archive powered by MhonArc 2.6.16.