-
Notifications
You must be signed in to change notification settings - Fork 299
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - chore(tactic/reserved_notation): change precedence of sup and inf #10623
Conversation
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Was using 71
and 72
too much refactoring work? I think that might be a better choice.
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Feel free to experiment with other values. I won't spend time on this. If you want to try 71 and 72 I can put this PR on hold until we decide what values we want. |
Let's merge this for now. If someone wants to revisit this later, this will still be possible, but this is already a net improvement over what we have currently. |
…0623) 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 Co-authored-by: Rémy Degenne <remydegenne@gmail.com>
Pull request successfully merged into master. Build succeeded: |
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