Stream: Coq users

Topic: Control printing?


view this post on Zulip 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?

view this post on Zulip Paolo Giarrusso (Aug 01 2020 at 17:31):

Something like "let x := eval cbv foo in idtac x" (or maybe eval cbv in foo ?)

view this post on Zulip Paolo Giarrusso (Aug 01 2020 at 17:31):

Tho you'll need to open a dummy goal first.


Last updated: Jan 28 2023 at 07:30 UTC