Zulip Chat Archive

Stream: Is there code for X?

Topic: rewrite at a specific variable?


view this post on Zulip 唐乾 (Aug 24 2020 at 19:25):

For example,I want to rw the rhs of"a+b=a" to "a+b=a+0"conveniently,what should I do?
I found that there is an intro. in
https://leanprover.github.io/tutorial/A1_Quick_Reference.html
which said"t at H {i, ...} : apply t only at numbered occurences in H"
but I don't know what is "i" means,and other ref. didn't explain this.

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:29):

The first line of this document says: "Note that this quick reference guide describes Lean 2 only. "

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:29):

Are you using Lean 2?

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:30):

If you don't know then the answer is no.

view this post on Zulip 唐乾 (Aug 24 2020 at 19:33):

oh! I'm using Lean 3,is there anyway in Lean 3?

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 19:34):

Yes, you can do targetted rewrites in several ways in Lean 3

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 19:35):

https://leanprover-community.github.io/extras/conv.html

view this post on Zulip Kyle Miller (Aug 24 2020 at 19:35):

example (a b : ) (h : a+b=a) : true :=
begin
  conv_rhs at h { rw nat.add_zero a },
end

(the true there is just a placeholder)

view this post on Zulip Patrick Massot (Aug 24 2020 at 19:44):

For the record, you can also do rw ← nat.add_zero a at h {occs := occurrences.pos [2]}, which is closer to what this ancient doc was referring to.

view this post on Zulip 唐乾 (Aug 24 2020 at 20:00):

thx!!It works !!!


Last updated: May 07 2021 at 21:10 UTC