Zulip Chat Archive

Stream: new members

Topic: rewriting only once


view this post on Zulip Xindi Ai (Jul 13 2019 at 13:52):

Hi all, is there a way to rewrite something only once? (E.g., when I need to rewrite something on one side of the equation only)
I found this option in the reference manual, which was for Lean 2, and it doesn't seem to work now.

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 14:01):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

view this post on Zulip Kevin Buzzard (Jul 13 2019 at 14:01):

That powerful tool should do the job, although there might be easier solutions in your particular case

view this post on Zulip Xindi Ai (Jul 13 2019 at 14:03):

https://github.com/leanprover-community/mathlib/blob/master/docs/extras/conv.md

Amazing. Thank you!


Last updated: May 17 2021 at 21:12 UTC