rewrite in one location only

Stream: new members

[Michael Beeson]

If an equation could be applied in two different locations and I want to rewrite at only one of them how do I accomplish that?

[Johan Commelin]

rw [foo, bar] { occs := occurence.pos [42] }

will only rewrite foo and bar at the 42nd occurence. (@Michael Beeson)

[Bryan Gin-ge Chen]

There are a few ways:

• There's a mathlib tactic nth_rewrite
• You can go into conv mode
• You can pass an occs option to rw (I don't fully understand the syntax, but see https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Sam.20Estep/near/201095954)

[Kevin Buzzard]

I can never remember the syntax for occs either, maybe it should be in the conv docs or maybe there should be a brief rewrite doc? Oh how about an occs example in the docstring for rw? Maybe that's the place for these hints?

[Bryan Gin-ge Chen]

I think the tactic doc entry for rw / rewrite would be a good spot. It would also be convenient to put in the docstrings for rw and rewrite, too.

[Damiano Testa]

@Johan Commelin just a small typo in your code: I liked it so much that I wanted to try it out!

rw [foo, bar] { occs := occurrences.pos [42] }

[Johan Commelin]

Thanks, I'll fix it.

[Scott Morrison]

Be careful --- occs will not work/count correctly if there are multiple places where an identical rewrite can occur. For this you need nth_rewrite.