Zulip Chat Archive

Stream: new members

Topic: see what simp did


view this post on Zulip Patrick Lutz (Jun 10 2020 at 23:55):

Is there a way to see what simp did? Sometimes there's something I know should be easy but I can't figure out what it's called in mathlib but I know simp will do it for me. But I've also read that I shouldn't use simp on nonterminal lines. So it would be nice if I could run simp and then check what simp was actually doing and replace it with that

view this post on Zulip Jalex Stark (Jun 10 2020 at 23:56):

there's squeeze_simp which solves the "replace it with what it did" problem

view this post on Zulip Bryan Gin-ge Chen (Jun 10 2020 at 23:57):

There's set_option trace.simplify.rewrite true. See https://leanprover-community.github.io/extras/simp.html for some more info.

view this post on Zulip Jalex Stark (Jun 10 2020 at 23:58):

This quite recent thread has a little more discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/tidy/near/199996920

view this post on Zulip Patrick Lutz (Jun 10 2020 at 23:59):

Wow, somehow I wasn't really aware of squeeze_simp

view this post on Zulip Johan Commelin (Jun 11 2020 at 00:58):

We should add it to the docstring of simp.

view this post on Zulip Johan Commelin (Jun 11 2020 at 01:00):

I don't have time right now: so I put it in an issue lean#316.


Last updated: May 06 2021 at 22:13 UTC