Zulip Chat Archive

Stream: new members

Topic: Where to rewrite

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?

Benjamin (Sep 08 2020 at 04:43):

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

Johan Commelin (Sep 08 2020 at 04:53):

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

Johan Commelin (Sep 08 2020 at 04:53):

@Benjamin :up:

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: Dec 20 2023 at 11:08 UTC