Lean4 infixl

Stream: new members

[vlado]

I was looking at the examples at https://leanprover.github.io/lean4/doc/notation.html and tried to chain infixl operator but keep getting an error:

infixr:65  " @ " => Div.div  -- right-associative
#eval 8 @ 4 @ 2 -- works 4 == (8 / (4 / 2))

infixl:65  " $ " => Div.div -- left-associative
#eval 8 $ 4 $ 2 -- error function expected at 8 term has type ?m.2645

The expanded notation did seem to work though

notation:65 lhs:65 " # " rhs:66 => Div.div lhs rhs -- left-associative
#eval 8 # 4 # 2 -- works 1 == ((8 / 4) / 2)

Am I doing something wrong in the infixl decleration or is this a bug?

[Henrik Böving]

I'd say this is because $ is already a reserved syntax for the Haskell style $ operator but I'm not 100 percent sure.

[vlado]

woops that was it, I tried both '$' and '@' and got the same error but '#' works, so must be using some other reserved operators. Thanks!

[Marcus Rossel]

@vlado Just FYI, there's also a lean4 stream here on Zulip.