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?
Something like "let x := eval cbv foo in idtac x" (or maybe eval cbv in foo ?)
Tho you'll need to open a dummy goal first.
Last updated: Oct 04 2023 at 21:01 UTC