How does associating a symbol to an operation works

Stream: general

[Esteban Martínez Vañó]

Hi everyone.

While reading Chapter 7 of Mathematics in Lean, there are several ways to associate to an operation a symbol.

For example:

class One₁ (α : Type) where
  /-- The element one -/
  one : α

@[inherit_doc]
notation "𝟙" => One₁.one

class Dia₁ (α : Type) where
  dia : α → α → α

infixl:70 " ⋄ " => Dia₁.dia


class Inv₁ (α : Type) where
  /-- The inversion function -/
  inv : α → α

@[inherit_doc]
postfix:max "⁻¹" => Inv₁.inv

class LE₁ (α : Type) where
  /-- The Less-or-Equal relation. -/
  le : α → α → Prop

@[inherit_doc] infix:50 " ≤₁ " => LE₁.le

class SMul₃ (α : Type) (β : Type) where
  /-- Scalar multiplication -/
  smul : α → β → β

infixr:73 " • " => SMul₃.smul

I guess, the first one is standard for constants, but how do the other ones work?
What is the number next to "infixl" or "infixr" and what's the difference between these two?
Why is it different for the inversion and the less and or equal relation?

[Chris Bailey]

There's more in-depth guidance/documentation for this specific question here: https://lean-lang.org/lean4/doc/notation.html

infixl and infixr desugar to notation. The numbers are used to control operator precedence. Precedence is how tightly each operator binds to its operands, and is the difference between a + b + c parsing as (a + b) + c and parsing as a + (b + c).

[Esteban Martínez Vañó]

Thank you!