leftarrow (←)

Stream: new members

[Hank]

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 :=
begin
rw ← add_assoc,
rw add_left_neg,
rw zero_add
end

[Bryan Gin-ge Chen]

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]

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]

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]

That's correct.

[Hank]

thanks!