# Zulip Chat Archive

## 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: Aug 03 2023 at 10:10 UTC