Stream: Coq users

Topic: Interactive computation unfolding?

view this post on Zulip Shea Levy (Oct 14 2020 at 18:48):

Is there any way (ideally with pg) to interactively unfold/compute terms in a definition? Usually I just use Compute vernacular but right now it's computing too much.

view this post on Zulip Enrico Tassi (Oct 14 2020 at 19:56):

the lazy reduction (Eval lazy in ...) takes many parameters, like what to unfold

view this post on Zulip Paolo Giarrusso (Oct 14 2020 at 20:48):

also cbv, cbn, simpl — there’s a long section in the manual

Last updated: Jun 15 2024 at 08:01 UTC