question about infix in tutorial

Stream: general

[Abhishek Cherath]

So I was going through the lean tutorial and I came across this line of code
infix ` is_a_max_of `:55 := is_max

What's the 55 mean?

[Alex J. Best]

It's a precedence number specifying the order of the notation over others.
https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#notation

[Abhishek Cherath]

Thanks! im still a bit confused though, does that mean if I redefine is_a_max_of but with priority 50 it'll use the older definition instead? or does it affect the order of reductions?

[Alex J. Best]

Its only about the order of operations.

def is_max ( n : ℕ) (m : set ℕ) :Prop := sorry
def is_max' ( n : ℕ) (m : set ℕ) :Prop := sorry
infix ` is_a_max_of `:55 := is_max
infix ` is_a_max_of `:50 := is_max'
#print is_a_max_of -- we can see that is_max' is used
set_option pp.notation false
#check (1 is_a_max_of {1,2}) -- we can see that is_max' is used
#check 1 + 2 is_a_max_of {1,2} -- this works as the priority of + is 65, #print +
infix ` is_a_max_of `:160 := is_max'
#check 1 + 2 is_a_max_of {1,2} -- error because now it tries to add 1 to the proposition that 2 is a max

[Kevin Buzzard]

It's priority in the following sense: https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/

[Mario Carneiro]

The proper term is "precedence" (parenthesis binding strength), not "priority" (preference of use in case of clashes)

[Abhishek Cherath]

Alex J. Best said:

Its only about the order of operations.

def is_max ( n : ℕ) (m : set ℕ) :Prop := sorry
def is_max' ( n : ℕ) (m : set ℕ) :Prop := sorry
infix ` is_a_max_of `:55 := is_max
infix ` is_a_max_of `:50 := is_max'
#print is_a_max_of -- we can see that is_max' is used
set_option pp.notation false
#check (1 is_a_max_of {1,2}) -- we can see that is_max' is used
#check 1 + 2 is_a_max_of {1,2} -- this works as the priority of + is 65, #print +
infix ` is_a_max_of `:160 := is_max'
#check 1 + 2 is_a_max_of {1,2} -- error because now it tries to add 1 to the proposition that 2 is a max

AHHHHHHHHHH i get it

[Abhishek Cherath]

Alex J. Best said:

i get it! thanks!

[Abhishek Cherath]

Mario Carneiro said:

The proper term is "precedence" (parenthesis binding strength), not "priority" (preference of use in case of clashes)

yea that's what I was confused about.