Stream: new members
Topic: View what simp applied
Spencer Killen (Jun 01 2020 at 03:02):
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 (Jun 01 2020 at 03:02):
You can use
squeeze_simp instead and it will print out a
simp only invocation with the same result
Spencer Killen (Jun 01 2020 at 03:05):
Awesome, thanks! :)
Bryan Gin-ge Chen (Jun 01 2020 at 03:06):
There are also some trace options you can read about here.
Spencer Killen (Jun 01 2020 at 03:10):
set_option trace.simplify true gave me a wonderfully huge list of failed attempts
Johan Commelin (Jun 01 2020 at 03:10):
Such is the life of a simplifier.
Reid Barton (Jun 01 2020 at 08:41):
set_option trace.simplify.rewrite true is the one you want.
Last updated: May 10 2021 at 00:31 UTC