Zulip Chat Archive

Stream: new members

Topic: Rewrite once even though there are two instances


view this post on Zulip Ben Nale (Aug 10 2020 at 23:08):

Let's say I have the expression (x+3) twice in my goal and I want to replace only one of them with (x+2+1). How do I do this?

view this post on Zulip Alex J. Best (Aug 10 2020 at 23:10):

you can use tactic#conv to focus in on the part of the goal you want to rewrite.

view this post on Zulip Jalex Stark (Aug 10 2020 at 23:25):

nth_rewrite is relevant, too, I think

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

You can also pass an occs option to rw: https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Sam.20Estep/near/201095954 but nth_rewrite is apparently better.


Last updated: May 14 2021 at 07:19 UTC