Zulip Chat Archive

Stream: general

Topic: Parsing left arrows


view this post on Zulip Rob Lewis (Feb 06 2019 at 12:27):

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

view this post on Zulip Johan Commelin (Feb 06 2019 at 12:31):

"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

view this post on Zulip Johan Commelin (Feb 06 2019 at 12:31):

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

view this post on Zulip Rob Lewis (Feb 06 2019 at 14:19):

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.

view this post on Zulip Rob Lewis (Feb 06 2019 at 14:20):

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


Last updated: May 17 2021 at 22:15 UTC