Commit 2021-12-12 21:34 19dd4be3
View on Github →chore(tactic/reserved_notation): change precedence of sup and inf (#10623)
Put the precedence of ⊔
and ⊓
at 68 and 69 respectively, which is above +
(65), ∑
and ∏
(67), and below *
(70). This makes sure that inf and sup behave in the same way in expressions where arithmetic operations appear (which was not the case before).
Discussion: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/inf.20and.20sup.20don't.20bind.20similarly