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.

hmm thanks

Last updated: Jun 16 2024 at 01:42 UTC