print the tactics simp is using?

Stream: new members

[Daniel Windham]

I'm trying to convert simp [...] to simp only [...]. How can I tell what tactics simp is using?

[Chris Bailey]

Try the new(ish) simp? [..]There's some info about it in these release notes: https://lean-lang.org/blog/2024-4-4-lean-470/

[Daniel Windham]

Perfect, thanks @Chris Bailey

[Chris Bailey]

There are also options for set_option under the trace prefix that have to do with the simplifier, but that's probably more than you want.

[Daniel Windham]

Got it, thanks. I saw someone use that before but simp? solves my problem.