Zulip Chat Archive

Stream: new members

Topic: rewrite in one location only


view this post on Zulip 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?

view this post on Zulip 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)

view this post on Zulip Bryan Gin-ge Chen (Oct 15 2020 at 04:54):

There are a few ways:

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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] }

view this post on Zulip Johan Commelin (Oct 15 2020 at 06:09):

Thanks, I'll fix it.

view this post on Zulip 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: May 06 2021 at 22:13 UTC