All Questions
1
question
6
votes
1
answer
405
views
How to evaluate proof terms through opaque definitions?
Is there is a way to force computation over opaque terms, for the purposes of debugging/meta-analysis of proof scripts.
I understand why Coq doesn’t do this by default, and guess it would probably ...
