Zulip Chat Archive

Stream: new members

Topic: leftarrow (←)

Hank (Dec 22 2021 at 05:48):

what does the leftarrow mean? Sometimes it is required in rewrites and sometimes it is not.

import algebra.ring

namespace my_ring

variables {R : Type*} [ring R]

theorem neg_add_cancel_left (a b : R) : -a + (a + b) = b :=
rw  add_assoc,
rw add_left_neg,
rw zero_add

Bryan Gin-ge Chen (Dec 22 2021 at 05:54):

Our tactic docs give the following explanation:

rw e applies an equation or iff e as a rewrite rule to the main goal. If e is preceded by left arrow ( or <-), the rewrite is applied in the reverse direction.

Does that answer your question?

Bryan Gin-ge Chen (Dec 22 2021 at 05:56):

It'd probably be good if we duplicated some of that information in the doc string for rw, since right now it just says "an abbreviation for rewrite" which isn't very convenient.

Stuart Presnell (Dec 22 2021 at 05:56):

So if you have h : x = y then rw h will turn x into y, and rw ← h will turn y into x

Bryan Gin-ge Chen (Dec 22 2021 at 05:58):

That's correct.

Hank (Dec 22 2021 at 05:59):


Last updated: Dec 20 2023 at 11:08 UTC