Alexander Gryzlov (Nov 04 2020 at 19:26): Alexander Gryzlov (Nov 04 2020 at 19:26):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?
Alexander Gryzlov (Nov 04 2020 at 19:28):I'm on 8.12 by the way.
Pierre-Marie Pédrot (Nov 04 2020 at 19:43):Have you tried the "Printing Depth" option?
Gaëtan Gilbert (Nov 04 2020 at 19:50):there's no way to go higher than the default depth AFAIK
Alexander Gryzlov (Nov 04 2020 at 22:36):yeah it doesn't look like changing it to more than 50 affects anything
Alexander Gryzlov (Nov 04 2020 at 22:36):is there maybe another way to export the term in a middle of a proof?
Paolo Giarrusso (Nov 04 2020 at 23:01):For a closing proof, there is abstract.
Paolo Giarrusso (Nov 04 2020 at 23:02):It doesn't sound like the proof is closing, but you could e.g. "rewrite (_ : a = b) by abstract rewrite ...". Probably painful.
Alexander Gryzlov (Nov 04 2020 at 23:08):hmm thanks
Last updated: Oct 13 2024 at 01:02 UTC