Zulip Chat Archive

Stream: new members

Topic: Rewrite once even though there are two instances

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?

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.

Jalex Stark (Aug 10 2020 at 23:25):

nth_rewrite is relevant, too, I think

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