Notation precedence

Stream: new members

[jsodd]

I haven't yet used notation feature, but I've read in Theorem Proving in Lean 4 that the number after colon stands for the precedence. Are there some guidelines for choosing this number? Is there some standard choice?

And, in general, is there a place where one can read more about such things?

[Kyle Miller]

For binary operators, one way to choose precedence is to think about whether this operator is used like another operator (maybe it's like a multiplication? or an addition? or a relation like equality?), and then you can look up that notation's definition to see what precedence it has.

More generally, you have to think about what sorts of expressions you will want to write with the notation and in different cases whether you would or would not expect to need to use parentheses. That helps guide you to an acceptable precedence. There are a number of cases of basic notations in mathlib getting precedences modified later when people realize its parenthesization is inconvenient.

[jsodd]

So the idea is to pick some already existing similar notation and take the same value.