trace of simp

Stream: new members

[Winston Yin]

Is there any way to find out which lemmas a particular simp used?

[Eric Rodriguez]

squeeze_simp or if that doesn't work (rarely) then simp?

[Eric Rodriguez]

there's also set_option simplifier.trace_rewrites true or something like that

[Eric Rodriguez]

and worst worst case, you can always wrap any tactic in show_term { ... } to see the term-mode proof it spat out

[Winston Yin]

Thanks!