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: finset.uIcc on concrete structures #5946

Closed
wants to merge 4 commits into from
Closed

[Merged by Bors] - feat: finset.uIcc on concrete structures #5946

wants to merge 4 commits into from

Conversation

YaelDillies
Copy link
Collaborator

@YaelDillies YaelDillies added awaiting-review The author would like community review of the PR mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Jul 16, 2023
eric-wieser
eric-wieser reviewed Jul 16, 2023
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.

I'll go over this in detail tomorrow.

Is there any reason you skipped data.finset.locally_finite? Also, that makes it seem like you somehow touched one extra file that wasn't on the dashboard, though I haven't checked off all 13 to work out which...

@eric-wieser eric-wieser self-assigned this Jul 16, 2023
@semorrison
Copy link
Contributor

@eric-wieser, the changes to data.finset.locally_finite are just whitespace. I'll bump the SHA.

@eric-wieser
Copy link
Member

Well now this touches 14 files but only 13 are on the dashboard! Which one is the extra one?

@semorrison
Copy link
Contributor

Mathlib/Data/Finset/Lattice.lean

See comment above. There's one file with an unnecessary SHA bump.

@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 Jul 17, 2023
bors bot pushed a commit that referenced this pull request Jul 17, 2023
@YaelDillies @semorrison
feat: finset.uIcc on concrete structures (#5946)
ae594c9 
Match leanprover-community/mathlib#18838




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

bors bot commented Jul 17, 2023

Pull request successfully merged into master.

Build succeeded!

The publicly hosted instance of bors-ng is deprecated and will go away soon.

If you want to self-host your own instance, instructions are here.
For more help, visit the forum.

If you want to switch to GitHub's built-in merge queue, visit their help page.

@bors bors bot changed the title feat: finset.uIcc on concrete structures [Merged by Bors] - feat: finset.uIcc on concrete structures Jul 17, 2023
@bors bors bot closed this Jul 17, 2023
@bors bors bot deleted the card_finset_interval branch July 17, 2023 03:51
semorrison added a commit that referenced this pull request Aug 14, 2023
@YaelDillies @semorrison
feat: finset.uIcc on concrete structures (#5946)
e2d9529 
Match leanprover-community/mathlib#18838




Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@eric-wieser eric-wieser eric-wieser left review comments

@semorrison semorrison semorrison left review comments

Assignees

@eric-wieser eric-wieser

Labels
mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged ready-to-merge This PR has been sent to bors.
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
3 participants
@YaelDillies @semorrison @eric-wieser