## Stream: general

### Topic: question about infix in tutorial

#### Abhishek Cherath (Nov 07 2020 at 06:50):

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 (Nov 07 2020 at 06:54):

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 (Nov 07 2020 at 06:58):

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 (Nov 07 2020 at 07:15):

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 (Nov 07 2020 at 07:17):

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

#### Mario Carneiro (Nov 07 2020 at 07:42):

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

#### Abhishek Cherath (Nov 07 2020 at 13:34):

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 (Nov 07 2020 at 13:34):

Alex J. Best said:

i get it! thanks!

#### Abhishek Cherath (Nov 07 2020 at 13:35):

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.

Last updated: Dec 20 2023 at 11:08 UTC