Zulip Chat Archive

Stream: new members

Topic: Applying rewrite to the nth match?

Christopher Hoskin (Mar 10 2021 at 20:41):

Sometimes I find myself trying to do something like rw ← add_zero a to replace a with a+0 in a goal. But I only want to do this for a particular occurrence of a in the goal, whereas rewrite replaces every occurrence. Is there a way to do this?



Bryan Gin-ge Chen (Mar 10 2021 at 20:43):

In mathlib there's nth_rewrite. There's also conv mode which is more powerful but often more verbose.

Christopher Hoskin (Mar 10 2021 at 20:45):

Thanks! nth_rewrite is just what I was looking for.

Last updated: Dec 20 2023 at 11:08 UTC