How does lean enforce associativity consistency

Stream: new members

[Shi Zhengyu]

Dear all,
How does Lean enforce operators of same precedence must have same associativity? Because notations in Lean can be manually specified left / right associativity on a per-notation basis, rather than per-precedence.
Thanks!

[Kevin Buzzard]

Lean keeps track of two binding powers for an infix notation; if these are equal the notation is left-associative and if the second is is one less than the first it's right associative.

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