Zulip Chat Archive

Stream: new members

Topic: Where to rewrite


view this post on Zulip Benjamin (Sep 08 2020 at 04:40):

I'm sure this is basic, but I can't figure this out from the documentation. How do I decide where to rewrite at a hypothesis? For example, if I want to rewrite the third instance of n to be n+0 in hypothesis h, what would I type?

view this post on Zulip Benjamin (Sep 08 2020 at 04:43):

What I've tried is rw \l add_zero(n) at h, but this replaces all instances.

view this post on Zulip Johan Commelin (Sep 08 2020 at 04:53):

rw [lemma1, lemma2] at hyp { occs := occurences.pos [3, 5] }

view this post on Zulip Johan Commelin (Sep 08 2020 at 04:53):

@Benjamin :up:

view this post on Zulip Benjamin (Sep 08 2020 at 04:56):

Thanks! Also, while I'm here, I know rw isn't supposed to be used for one way implications. Is there a function to use for that instead besides have, which requires creating another hypothesis?


Last updated: May 10 2021 at 19:16 UTC