## Stream: new members

### Topic: infix

#### Pedro Castilho (Nov 09 2020 at 20:46):

am reading leans tutorial and the code uses an infix of a definition to abbreviate the code but I don't get way an arbitrary number shows up while defining the infix

def is_inf (x : ℝ) (A : set ℝ) := x is_a_max_of (low_bounds A)
infix  is_an_inf_of :55 := is_inf


why is this "55" there?

#### Kevin Buzzard (Nov 09 2020 at 20:48):

it's operator precedence. https://xenaproject.wordpress.com/2019/01/20/a-word-on-bidmas/

#### Pedro Castilho (Nov 09 2020 at 20:55):

so its the power of the operator right? that makes a lot of sense now, probably best that I don't chance it than haha

#### Pedro Castilho (Nov 09 2020 at 20:56):

thx @Kevin Buzzard , btw I was in your lecture at fgv a few days ago, really liked it!

Last updated: May 13 2021 at 05:21 UTC