-
Notifications
You must be signed in to change notification settings - Fork 415
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
feat: set priority in monadic class instances #5291
base: master
Are you sure you want to change the base?
Conversation
Mathlib CI status (docs):
|
The test that broke had the number from the name generator offset by 8. |
Mathlib CI status (docs):
|
Mathlib CI status (docs):
|
Mathlib CI status (docs):
|
Mathlib CI status (docs):
|
!bench |
Here are the benchmark results for commit 90ac0f7. Benchmark Metric Change
========================================
- rbmap task-clock 2.2% (23.0 σ)
- rbmap wall-clock 2.3% (24.8 σ) |
I added the
high
priority to these instances with monad transformersI added the
low
priority to this instance with a monad transformerMonadExceptOf Unit (OptionT m)
.I added the
low
priority toMonadExcept.instOrElse
, because it needs to have lower priority thaninstOrElseOfAlternative
(this change doesn't affect the synthesis order, because the order of the files in which the instances were declared was already 'correct').In Prelude.lean, instead of setting the priority to
high
orlow
, I had to set it to10000
or100
, which is the same.The increased priority of
MonadExceptOf ε (ExceptT ε m)
affected a few files that had to be fixed.Closes #4212