Zulip Chat Archive

Stream: new members

Topic: see what simp did

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

Jalex Stark (Jun 10 2020 at 23:56):

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

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.

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

Patrick Lutz (Jun 10 2020 at 23:59):

Wow, somehow I wasn't really aware of squeeze_simp

Johan Commelin (Jun 11 2020 at 00:58):

We should add it to the docstring of simp.

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: Dec 20 2023 at 11:08 UTC