The Coq mailing list

[Georges Gonthier <gonthier AT microsoft.com>]

  Evaluation is guaranteed to terminate, but not necessarily in your 
lifetime...
If the definition you rendered opaque is a test performed by your recursive 
function before the recursive calls, for instance, I would expect the 
behaviour you describe: because it is unable to evaluate the test, Eval 
unfolds the complete branching tree, which is exponential in the size of the 
recursion depth -- and in practice, exponential is pretty much the same thing 
as infinite.

  -- Georges

-----Original Message-----
From: Vladimir Voevodsky 
[mailto:vladimir AT ias.edu]
 
Sent: 28 October 2010 19:26
To: Coq Club
Subject: [Coq-Club] strange behavior of "Eval compute"

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.