Shea Levy (Oct 14 2020 at 18:48): 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.
Enrico Tassi (Oct 14 2020 at 19:56):the lazy reduction (Eval lazy in ...) takes many parameters, like what to unfold
Paolo Giarrusso (Oct 14 2020 at 20:48):also cbv, cbn, simpl — there’s a long section in the manual
Last updated: Oct 05 2023 at 02:01 UTC