Michael Greenberg (Jul 31 2020 at 18:13): Michael Greenberg (Jul 31 2020 at 18:13):I'm using Compute to write a simple grader for assignments that are programs written in Coq (no proofs at this point in the course). Is there a way to have printing not emit the result types?
Paolo Giarrusso (Aug 01 2020 at 17:31):Something like "let x := eval cbv foo in idtac x" (or maybe eval cbv in foo ?)
Paolo Giarrusso (Aug 01 2020 at 17:31):Tho you'll need to open a dummy goal first.
Last updated: Oct 13 2024 at 01:02 UTC