Zulip Chat Archive

Stream: new members

Topic: rewrite in one location only

Michael Beeson (Oct 15 2020 at 04:50):

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 (Oct 15 2020 at 04:54):

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

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

Bryan Gin-ge Chen (Oct 15 2020 at 04:54):

There are a few ways:

Kevin Buzzard (Oct 15 2020 at 06:00):

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 (Oct 15 2020 at 06:03):

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 (Oct 15 2020 at 06:07):

@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 (Oct 15 2020 at 06:09):

Thanks, I'll fix it.

Scott Morrison (Oct 15 2020 at 10:33):

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.

Last updated: Dec 20 2023 at 11:08 UTC