55 in real numbers game

Stream: Berkeley Lean Seminar

[Rahul Dalal]

What does the 55 do here?
infix is_a_max_of:55 := is_max

[Pedro Minicz]

:55 is a precedence annotation if I am not mistaken.

[Patrick Lutz]

It's for order of operations

[Pedro Minicz]

Written without spaces around not to be confused with the typing :.

[Kyle Miller]

Avery Morin on the Zoom chat pointed out this documentation: https://leanprover.github.io/theorem_proving_in_lean/interacting_with_lean.html#notation

[Rahul Dalal]

is 55 a good default to usually use for consistent style?

[Pedro Minicz]

It depends on the precedence assigned to the other operators. We want things like a * b + c to be parsed as we would usually interpret it. So, it depends.

[Pedro Minicz]

The best practice would be to see whatever mathlib does and stick with it, I believe.

[K Y]

(deleted)