Zulip Chat Archive

Stream: new members

Topic: View what simp applied


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Spencer Killen (Jun 01 2020 at 03:05):

Awesome, thanks! :)

view this post on Zulip Bryan Gin-ge Chen (Jun 01 2020 at 03:06):

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

view this post on Zulip Spencer Killen (Jun 01 2020 at 03:10):

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

view this post on Zulip Johan Commelin (Jun 01 2020 at 03:10):

Such is the life of a simplifier.

view this post on Zulip 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