View what simp applied

Stream: new members

[Spencer Killen]

After I use the simp tactic, or any tactic for that matter, is there an easy way in interactive mode to view which rules were applied?

[Mario Carneiro]

You can use squeeze_simp instead and it will print out a simp only invocation with the same result

[Spencer Killen]

Awesome, thanks! :)

[Bryan Gin-ge Chen]

There are also some trace options you can read about here.

[Spencer Killen]

Haha thanks, set_option trace.simplify true gave me a wonderfully huge list of failed attempts

[Johan Commelin]

Such is the life of a simplifier.

[Reid Barton]

set_option trace.simplify.rewrite true is the one you want.