Zulip Chat Archive

Stream: Berkeley Lean Seminar

Topic: 55 in real numbers game


view this post on Zulip Rahul Dalal (May 26 2020 at 20:23):

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

view this post on Zulip Pedro Minicz (May 26 2020 at 20:24):

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

view this post on Zulip Patrick Lutz (May 26 2020 at 20:24):

It's for order of operations

view this post on Zulip Pedro Minicz (May 26 2020 at 20:24):

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

view this post on Zulip Kyle Miller (May 26 2020 at 20:25):

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

view this post on Zulip Rahul Dalal (May 26 2020 at 20:26):

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

view this post on Zulip Pedro Minicz (May 26 2020 at 20:28):

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.

view this post on Zulip Pedro Minicz (May 26 2020 at 20:28):

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

view this post on Zulip K Y (Jun 02 2020 at 19:56):

(deleted)


Last updated: May 06 2021 at 01:57 UTC