I want to debug a complex SSR rewrite rule by inspecting the proof term before and after its application to see which individual steps were applied. However the proof terms are several k lines long and
Show Proof starts replacing the output by
... at some particular nesting depth, hiding some of the latter steps. Is there a way to force it to spit out the full term without shortening?
I'm on 8.12 by the way.
Have you tried the "Printing Depth" option?
there's no way to go higher than the default depth AFAIK
yeah it doesn't look like changing it to more than 50 affects anything
is there maybe another way to export the term in a middle of a proof?
For a closing proof, there is abstract.
It doesn't sound like the proof is closing, but you could e.g. "rewrite (_ : a = b) by abstract rewrite ...". Probably painful.
Last updated: Feb 01 2023 at 11:04 UTC