Overload notation

Stream: lean4

[Marcus Rossel]

The following snippet fails:

axiom add : Nat → Nat → Nat
variable (x y : Nat)
infixl:65 " + " => add
#check x + y

/- ambiguous, possible interpretations
  x + y : Nat

  x + y : ?m.1776
-/

How can I force Lean to use my overload?

[Leonardo de Moura]

You can increase the parser priority

infixl:65 (priority := high) " + " => add

or

infixl:65 (priority := default+1) " + " => add

since the builtin notation uses the default priority