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] - chore: split Subsingleton,Nontrivial off of Data.Set.Basic #11832

Closed
wants to merge 28 commits into from
Closed

[Merged by Bors] - chore: split Subsingleton,Nontrivial off of Data.Set.Basic #11832

wants to merge 28 commits into from

Conversation

BoltonBailey
Copy link
Collaborator

@BoltonBailey BoltonBailey commented Apr 1, 2024 •
edited

Moves definition of and lemmas related to Set.Subsingleton and Set.Nontrivial to a new file, so that Basic can be shorter.

Open in Gitpod

@BoltonBailey BoltonBailey added the awaiting-author A reviewer has asked the author a question or requested changes label Apr 1, 2024
@BoltonBailey BoltonBailey added awaiting-author A reviewer has asked the author a question or requested changes awaiting-CI and removed awaiting-author A reviewer has asked the author a question or requested changes labels Apr 2, 2024
@BoltonBailey BoltonBailey removed the awaiting-author A reviewer has asked the author a question or requested changes label Apr 2, 2024
@BoltonBailey BoltonBailey added the awaiting-review The author would like community review of the PR label Apr 2, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot added merge-conflict The PR has a merge conflict with master, and needs manual merging. and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Apr 5, 2024
@leanprover-community-mathlib4-bot leanprover-community-mathlib4-bot removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Apr 10, 2024
@Ruben-VandeVelde
Copy link
Collaborator

It seems a bit weird to separate Set.Subsingleton and Set.Nontrivial

@BoltonBailey
Copy link
Collaborator Author

BoltonBailey commented Apr 11, 2024 •
edited

Good point. Nontrivial seems to not interfere with the rest of Basic so I have now moved that too. Any preference on the name for the new file then? (I'll just leave the name as Subsingleton.lean, let me know if you have a strong preference)

@BoltonBailey BoltonBailey changed the title chore: split Subsingleton off of Data.Set.Basic chore: split Subsingleton,Nontrivial off of Data.Set.Basic Apr 11, 2024
@BoltonBailey BoltonBailey added the tech debt tracking cross-cutting technical debt label Apr 13, 2024
@semorrison
Copy link
Contributor

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Apr 18, 2024
mathlib-bors bot pushed a commit that referenced this pull request Apr 18, 2024
@BoltonBailey
chore: split Subsingleton,Nontrivial off of Data.Set.Basic (#11832)
493a947 
Moves definition of and lemmas related to `Set.Subsingleton` and `Set.Nontrivial` to a new file, so that `Basic` can be shorter.
@mathlib-bors
Copy link

mathlib-bors bot commented Apr 18, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title chore: split Subsingleton,Nontrivial off of Data.Set.Basic [Merged by Bors] - chore: split Subsingleton,Nontrivial off of Data.Set.Basic Apr 18, 2024
@mathlib-bors mathlib-bors bot closed this Apr 18, 2024
@mathlib-bors mathlib-bors bot deleted the BoltonBailey/set-subsingleton-split branch April 18, 2024 06:50
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@BoltonBailey @uniwuni
chore: split Subsingleton,Nontrivial off of Data.Set.Basic (#11832)
39b78cc 
Moves definition of and lemmas related to `Set.Subsingleton` and `Set.Nontrivial` to a new file, so that `Basic` can be shorter.
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@BoltonBailey @callesonne
chore: split Subsingleton,Nontrivial off of Data.Set.Basic (#11832)
cd2342f 
Moves definition of and lemmas related to `Set.Subsingleton` and `Set.Nontrivial` to a new file, so that `Basic` can be shorter.
Jun2M pushed a commit that referenced this pull request Apr 24, 2024
@BoltonBailey @Jun2M
chore: split Subsingleton,Nontrivial off of Data.Set.Basic (#11832)
f4fcee5 
Moves definition of and lemmas related to `Set.Subsingleton` and `Set.Nontrivial` to a new file, so that `Basic` can be shorter.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers
No reviews
Assignees
No one assigned
Labels
ready-to-merge This PR has been sent to bors. tech debt tracking cross-cutting technical debt
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@BoltonBailey @Ruben-VandeVelde @semorrison @leanprover-community-mathlib4-bot