Stream: new members
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