Parsing left arrows

Stream: general

[Rob Lewis]

What magic is going on here? parser.tk "<-" is willing to consume a unicode left arrow, but parser.tk "←" isn't?

meta def tactic.interactive.what (_ : interactive.parse (lean.parser.tk "←")) : tactic unit :=
tactic.skip

meta def tactic.interactive.what2 (_ : interactive.parse (lean.parser.tk "<-")) : tactic unit :=
tactic.skip

example : true :=
begin
  what2 ←, -- works
  what ←,  -- fails
end

[Johan Commelin]

"Lean does not do magic" -- K. Lau, a couple of months ago

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/rw.20under.20a.20union/near/126557131

[Johan Commelin]

@Kenny Lau Voila, some homework for you :grinning:

[Rob Lewis]

Close enough to dark magic for my tastes. The token for ← is hardcoded to be an alias for <-. But the case I compared it with goes the other way around: (| is an alias for ⟨. So you can parse angle brackets just fine, but for left arrows, you'd better use ascii.

[Rob Lewis]

I think this line is redundant, then, which was a red herring. https://github.com/leanprover/lean/blob/master/library/init/meta/interactive.lean#L351