Definition foo := Eval lazy in addn 2 3. Extraction foo.
?
Thanks! That did it.
I haven't used lazy
before. Is it same as cbn
? Both are placed together in the docs: https://coq.inria.fr/refman/proofs/writing-proofs/equality.html#coq:tacn.lazy
Oh, sorry. They are explained there itself.
With lazy
, computation can be 'shared'. I guess that means the term is shared and all its usages get evaluated when the shared term is evaluated.
Julin Shaji has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC