Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC