-
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(data/option/defs): Swap arguments to option.elim
#14681
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.
Can you change option.melim
to match?
There wasn't any objection on Zulip, so
bors d+
✌️ YaelDillies can now approve this pull request. To approve and merge a pull request, simply reply with |
Did I not do that already? |
Well your PR description doesn't mention it! |
Fair. bors merge |
Make `option.elim` a non-dependent version of `option.rec` rather than a non-dependent version of `option.rec_on`. Same for `option.melim`. This replaces `option.cons`, and brings `option.elim` in line with `nat.elim`, `sum.elim`, and `iff.elim`. It addresses the TODO comment added in 22c4291.
Pull request successfully merged into master. Build succeeded: |
option.elim
option.elim
Make
option.elim
a non-dependent version ofoption.rec
rather than a non-dependent version ofoption.rec_on
. Same foroption.melim
.This replaces
option.cons
, and bringsoption.elim
in line withnat.elim
,sum.elim
, andiff.elim
.It addresses the TODO comment added in 22c4291.
Zulip