Skip to content
This repository has been archived by the owner on Jul 24, 2024. It is now read-only.

[Merged by Bors] - feat(set_theory/cardinal/basic): Inline instances #14130

Closed
wants to merge 8 commits into from
Closed

[Merged by Bors] - feat(set_theory/cardinal/basic): Inline instances #14130

wants to merge 8 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented May 13, 2022

We inline some instances, thus avoiding redundant lemmas. We also clean up the code somewhat.

Open in Gitpod

@vihdzp vihdzp added awaiting-review The author would like community review of the PR awaiting-CI The author would like to see what CI has to say before doing more work. labels May 13, 2022
@vihdzp vihdzp changed the title feat(set_theory/cardinal): Inline instances feat(set_theory/cardinal/basic): Inline instances May 13, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 13, 2022
@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels May 15, 2022
@vihdzp vihdzp added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels May 15, 2022
eric-wieser
eric-wieser approved these changes May 23, 2022
View reviewed changes
Copy link
Member

@eric-wieser eric-wieser left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

bors d+

@bors
Copy link

bors bot commented May 23, 2022

✌️ vihdzp can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

@leanprover-community-bot-assistant leanprover-community-bot-assistant added delegated The PR author may merge after reviewing final suggestions. and removed awaiting-review The author would like community review of the PR labels May 23, 2022
@vihdzp vihdzp added the awaiting-CI The author would like to see what CI has to say before doing more work. label May 23, 2022
@github-actions github-actions bot removed the awaiting-CI The author would like to see what CI has to say before doing more work. label May 23, 2022
@vihdzp
Copy link
Collaborator Author

vihdzp commented May 23, 2022

bors r+

bors bot pushed a commit that referenced this pull request May 23, 2022
@vihdzp
feat(set_theory/cardinal/basic): Inline instances (#14130)
3f0a2bb 
We inline some instances, thus avoiding redundant lemmas. We also clean up the code somewhat.
@bors
Copy link

bors bot commented May 23, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(set_theory/cardinal/basic): Inline instances [Merged by Bors] - feat(set_theory/cardinal/basic): Inline instances May 23, 2022
@bors bors bot closed this May 23, 2022
@bors bors bot deleted the cardinal_inline branch May 23, 2022 22:05
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.
Reviewers

@urkud urkud urkud left review comments

@eric-wieser eric-wieser eric-wieser approved these changes

Assignees
No one assigned
Labels
delegated The PR author may merge after reviewing final suggestions.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
4 participants
@vihdzp @urkud @eric-wieser @leanprover-community-bot-assistant