Priority of notation

Stream: general

[Antoine Chambert-Loir]

I have defined a notation

notation:25 α " →[" M:25 "] " β:0 => EquivariantMap (@id M) α β

which conflicts with the one for MulActionHom. Because of that ambiguity, Lean stops.
I tried to insert (priority := 1000) , without success…
How can I make mine to be chosen automatically?

[Eric Wieser]

I think 1000 is the default priority so providing that won't do anything

[Antoine Chambert-Loir]

By without success, I meant that I got an error message.
Where should I insert the priority attribute? I tried notation (priority := 1000) :25…

[Junyan Xu]

Many examples are found by searching the repo, for example this. M:25 β:0 don't feel right to me ... Oops it's used here.

[Eric Wieser]

:25 is precedence not priority

[Junyan Xu]

What does it mean to put a precedence on a variable?

[Kyle Miller]

@Antoine Chambert-Loir I believe the priority goes after the :25.

[Kyle Miller]

Just to confirm, here is the syntax definition for notation.

Here's what that means using simplified syntax-like notation:

(docComment)? (attributes)? attrKind
"notation" (precedence)? (namedName)? (namedPrio)? notationItem* "=>" term

The attrKind is ("scoped" <|> "local")?, the namedName is "(name :=" ident ")", and the namedPrio is "(priority :=" priority ")".

[Kyle Miller]

The priority parser has a number of named priority levels by the way. There's default, low, mid, and high, and you can write expressions involving +, -, and parentheses.