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] - refactor(data/set/basic): Adds inter_nonempty to match union_nonempty. #14854

Closed
wants to merge 5 commits into from
Closed

[Merged by Bors] - refactor(data/set/basic): Adds inter_nonempty to match union_nonempty. #14854

wants to merge 5 commits into from

Conversation

linesthatinterlace
Copy link
Collaborator

@linesthatinterlace linesthatinterlace commented Jun 20, 2022 •
edited

Also changes existing inter_nonempty lemmas to match.

@linesthatinterlace linesthatinterlace 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 Jun 20, 2022
@eric-wieser
Copy link
Member

I'm struggling to spot the new coercions here, as they're hiding among the style changes. I also don't think that changing things from a single .imp to a pile of ⟨_⟩ is really an improvement...

@linesthatinterlace
Copy link
Collaborator Author

It's in the first commit - I'm happy to drop the second one if you don't like the style.

@linesthatinterlace
Copy link
Collaborator Author

@eric-wieser were you OK with the first commit?

@linesthatinterlace
Copy link
Collaborator Author

Removed unwanted proof changes; this should also have fixed the merge issues.

@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 Jul 5, 2022
@urkud
Copy link
Member

urkud commented Jul 12, 2022

@eric-wieser Could you please have another look? I'm OK with changing the two lemmas (or, e.g., adding new versions and preserving the old ones as ...').

@linesthatinterlace
Copy link
Collaborator Author

I'm happy to do either of those, @urkud.

@linesthatinterlace
Copy link
Collaborator Author

What am I doing with this?

@urkud
Copy link
Member

urkud commented Jul 24, 2022

Waiting for @eric-wieser . You can try pinging him on Zulip.

@eric-wieser
Copy link
Member

@urkud, I'm happy for you to make a call on this

eric-wieser
eric-wieser reviewed Aug 1, 2022
View reviewed changes
src/topology/basic.lean Outdated Show resolved Hide resolved
@linesthatinterlace linesthatinterlace changed the title refactor(data/set/basic): Modify inter nonempty lemmas. refactor(data/set/basic): Adds inter_nonempty to match union_nonempty. Aug 1, 2022
jcommelin
jcommelin approved these changes Aug 15, 2022
View reviewed changes
Copy link
Member

@jcommelin jcommelin left a comment

Choose a reason for hiding this comment

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

Thanks 🎉

bors merge

@leanprover-community-bot-assistant leanprover-community-bot-assistant added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Aug 15, 2022
@jcommelin
Copy link
Member

bors merge p=3

bors bot pushed a commit that referenced this pull request Aug 15, 2022
@linesthatinterlace
refactor(data/set/basic): Adds inter_nonempty to match `union_nonem…
8cd4f19 
…pty`. (#14854)

Also changes existing `inter_nonempty` lemmas to match.



Co-authored-by: Wrenna Robson <34025592+linesthatinterlace@users.noreply.github.com>
@bors
Copy link

bors bot commented Aug 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(data/set/basic): Adds inter_nonempty to match union_nonempty. [Merged by Bors] - refactor(data/set/basic): Adds inter_nonempty to match union_nonempty. Aug 16, 2022
@bors bors bot closed this Aug 16, 2022
@bors bors bot deleted the nonempty_inter_iff branch August 16, 2022 01:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@urkud urkud urkud left review comments

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

@jcommelin jcommelin jcommelin approved these changes

Assignees

@urkud urkud

Labels
ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.)
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
5 participants
@linesthatinterlace @eric-wieser @urkud @jcommelin @leanprover-community-bot-assistant