Stream: new members
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: May 14 2021 at 07:19 UTC