Notation precedence

Stream: lean4

[Marcus Rossel]

Is there an overview somewhere of the precedences used in various notations in Lean?

I'm hoping that this might help me understand the notation macro a bit better. I still have problems understanding the statement from Lean Manual > Notations and Precedence:

A placeholder with precedence p accepts only notations with precedence at least p in that place. Thus the string a + b + c cannot be parsed as the equivalent of a + (b + c)

.. where: notation:65 lhs:65 " + " rhs:66 => HAdd.hAdd lhs rhs

Does notation:65 mean that a term of the form <lhs> + <rhs> will have a precedence of 65?
And hence, since rhs has precedence 66, it will not accept a term of the form <lhs> + <rhs>.
But since lhs has precedence 65 it will, and hence + associates to the left?

[Kevin Buzzard]

In Lean 3,

#print notation + -- _ `+`:65 _:65 := has_add.add #1 #0

means nothing more or less than "+ is an infix operator which is left associative and has binding power 65", and

#print notation ^ -- _ `^`:80 _:79 := has_pow.pow #1 #0

means that ^ is an infix operator which is right associative and has binding power 80. You can read off left or right associativity by noting whether the second number is equal to the first, or one less. To find out why all this works you can read about Pratt parsing but at the end of the day the rule of thumb above is all I've ever needed.

[Chris B]

For regular infix operators, Pratt parsers just need a left and right number, though it's common to just take one and turn left associative operators into (n, op, n+1) and right-associative ones into (n+1, op, n). The number after notation just seems to be a way of controlling whether and when associativity/chaining of certain operators is even allowed. The example they give is:

notation:50 lhs:51 " = " rhs:51 => Eq lhs rhs

In the context of the "A placeholder with precedence p..." statement, the point of notation:50 relative to the lbp/rbp is that this notation can't be chained since it doesn't associate in either direction. This throws an error:

example : 1 = 2 = 3 := sorry