Inspecting simp

Stream: new members

[Bbbbbbbbba]

Is there a way to see what simp is actually doing?

[llllvvuu]

Bbbbbbbbba said:

Is there a way to see what simp is actually doing?

simp? for the lemmas it used

set_option trace.Meta.Tactic.simp true for the lemmas it tried but couldn't use

[Bbbbbbbbba]

llllvvuu said:

Bbbbbbbbba said:

Is there a way to see what simp is actually doing?

simp? for the lemmas it used

set_option trace.Meta.Tactic.simp true for the lemmas it tried but couldn't use

This is helpful, although I was thinking of something like turning a tactic-style proof to a completely term-style proof (so that it becomes insensitive to the simp algorithm)

[Mauricio Collares]

You can always use show_term { simp }, but the proof is likely not very human-readable.

[llllvvuu]

You can also #print the entire declaration. Note that while term-mode proof is less sensitive to tactic implementations, it's more sensitive to individual lemmas and other things, so overall it may not be less prone to breakage

[Bbbbbbbbba]

I see, thanks!

[Joachim Breitner]

There is also this little, still somewhat experimental tool that expands a simp proof into an elaborate calc proof:
https://github.com/nomeata/lean-calcify