The Coq mailing list

[roconnor AT theorem.ca]

You may also want to try

Eval lazy beta delta iota zeta in ...

which can work well in some situations where you have a big computation 
that gets thrown away anyways.

On Thu, 28 Oct 2010, Georges Gonthier wrote:

>  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.

--
Russell O'Connor                                      <http://r6.ca/>
``All talk about `theft,''' the general counsel of the American Graphophone
Company wrote, ``is the merest claptrap, for there exists no property in
ideas musical, literary or artistic, except as defined by statute.''