infix

Stream: new members

[Pedro Castilho]

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]

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

[Pedro Castilho]

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]

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