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