Skip to content
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.

Sign up for GitHub

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

Jump to bottom

[Merged by Bors] - feat: port Data.Option.Basic #493

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - feat: port Data.Option.Basic #493

wants to merge 28 commits into from

Conversation

pechersky
Copy link
Collaborator

  • Define getOrElse here -- likely belongs in Std
  • lemmas mentioning coe now use up-arrow, even though that refers to some directly
  • Option.elim has different argument order

@digama0
Copy link
Member

digama0 commented Oct 24, 2022

#align option.get_or_else Option.getD

@digama0
Copy link
Member

digama0 commented Oct 24, 2022

One trick to handle the Option.elim reorder is to use #align option.elim Option.elimₓ. This will make lean treat it formally as a separate definition so it won't get too confused with type errors resulting from literally using Option.elim for option.elim, but during printing it will remove the ₓ which should usually be fine as long as the definition is applied with dot-notation where it's the same either way. (You should put a comment on the #align to explain what changed though.)

@pechersky
Copy link
Collaborator Author

Can you give some guidance on what to do about all the simp lemmas that are now either replicated elsewhere, or the ones that now simpify on the LHS? I've commented out the simp tags to appease the linter.

@javra javra mentioned this pull request Oct 25, 2022
Closed
javra
javra reviewed Oct 25, 2022
View reviewed changes
Mathlib/Init/Logic.lean Outdated Show resolved Hide resolved
@pechersky pechersky added blocked-by-other-PR This PR depends on another PR to Mathlib awaiting-author A reviewer has asked the author a question or requested changes and removed blocked-by-other-PR This PR depends on another PR to Mathlib awaiting-review labels Oct 26, 2022
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review labels Nov 1, 2022
@pechersky
Clean up based on comments
09cb9a0 
Aligns remove a lot of leftover lemmas that are in Std
One lemma can't get simp-tagged because of a LHS simplification issue
@pechersky pechersky added awaiting-review blocked-by-other-PR This PR depends on another PR to Mathlib and removed awaiting-author A reviewer has asked the author a question or requested changes labels Nov 2, 2022
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR to Mathlib and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Nov 2, 2022
@semorrison
Copy link
Contributor

I've merged the combinators PR now. Could you update this to reflect that?

@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed blocked-by-other-PR This PR depends on another PR to Mathlib labels Nov 6, 2022
@pechersky pechersky removed the awaiting-author A reviewer has asked the author a question or requested changes label Nov 6, 2022
@semorrison
Copy link
Contributor

bors merge

bors bot pushed a commit that referenced this pull request Nov 7, 2022
@pechersky @semorrison
feat: port Data.Option.Basic (#493)
fd97e04 
- Define `getOrElse` here -- likely belongs in `Std`
- lemmas mentioning `coe` now use up-arrow, even though that refers to `some` directly
- `Option.elim` has different argument order

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link

bors bot commented Nov 7, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Data.Option.Basic [Merged by Bors] - feat: port Data.Option.Basic Nov 7, 2022
@bors bors bot closed this Nov 7, 2022
@bors bors bot deleted the pechersky/port-option-basic branch November 7, 2022 04:25
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@javra javra javra left review comments

@semorrison semorrison semorrison left review comments

@digama0 digama0 digama0 left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@pechersky @digama0 @semorrison @javra