I was wondering if 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 interact in unfavourable ways with proof irrelevance.
My aim is not to use this computation as part of a proof, but rather purely for debugging/meta-analysis - much like how the Print command can display the proof terms associated with lemmas, even if they are actually opaque.
Is it possible, using the Coq api if necassary, to perform computation ignoring opaqueness of terms? Think something like a PrintReduced command that reduces its argument as much as possible (until it reaches constructors, existential variables or axioms - things for which the definition doesn’t exist at all)?
Is this possible while reusing Coq’s existing evaluation mechanisms? or is this something that would require a much larger architectural shift?