Stream: Coq users

Topic: ✔ Extract only computed value


view this post on Zulip Gaëtan Gilbert (Oct 28 2023 at 16:04):

Definition foo := Eval lazy in addn 2 3. Extraction foo. ?

view this post on Zulip Julin Shaji (Oct 28 2023 at 16:19):

Thanks! That did it.

view this post on Zulip Julin Shaji (Oct 28 2023 at 16:21):

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

view this post on Zulip Julin Shaji (Oct 28 2023 at 16:21):

Oh, sorry. They are explained there itself.

view this post on Zulip Julin Shaji (Oct 28 2023 at 16:23):

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.

view this post on Zulip Notification Bot (Oct 28 2023 at 16:37):

Julin Shaji has marked this topic as resolved.


Last updated: Oct 13 2024 at 01:02 UTC