-
Notifications
You must be signed in to change notification settings - Fork 297
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] - refactor(*): use option.map₂
#18081
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.
Nice PR! I had seen some of those definitions and thought it would be an improvement to use data.option.n_ary
, so I approve!
…athlib into YK-opt-map2
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.
bors d+
I added a handful more id $
s, and moved the explanation of their purpose to the module docstring.
Can you make sure you forward port these if appropriate?
✌️ urkud can now approve this pull request. To approve and merge a pull request, simply reply with |
Thanks! bors merge I don't think that we need this in Mathlib 4 because we don't (and can't) use the "make it irreducible later" trick with Lean 4. |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
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.
Sorry, last minute typo!
Canceled. |
bors merge |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed (retrying...): |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed (retrying...): |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed (retrying...): |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Build failed (retrying...): |
Relevant parts are forward-ported as leanprover-community/mathlib4#1439 Co-authored-by: Eric Wieser <wieser.eric@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>
Pull request successfully merged into master. Build succeeded: |
option.map₂
option.map₂
This is a forward-port of leanprover-community/mathlib#18081
Relevant parts are forward-ported as leanprover-community/mathlib4#1439