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(order/extension): extend partial order to linear order #7142

Closed
wants to merge 17 commits into from
Closed

[Merged by Bors] - feat(order/extension): extend partial order to linear order #7142

wants to merge 17 commits into from

Conversation

b-mehta
Copy link
Collaborator

@b-mehta b-mehta commented Apr 9, 2021 •
edited

Adds a construction to extend a partial order to a linear order. Also fills in a missing Zorn variant.

Open in Gitpod

@b-mehta b-mehta added the awaiting-review The author would like community review of the PR label Apr 9, 2021
@github-actions github-actions bot added the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 9, 2021
@github-actions github-actions bot removed the merge-conflict Please `git merge origin/master` then a bot will remove this label. label Apr 9, 2021
@bryangingechen bryangingechen changed the title feat(order): extend partial order to linear order feat(order/extension): extend partial order to linear order Apr 10, 2021
@b-mehta b-mehta added WIP Work in progress and removed awaiting-review The author would like community review of the PR labels Apr 10, 2021
@b-mehta
Copy link
Collaborator Author

b-mehta commented Apr 10, 2021

I'm switching this back to WIP for now since I think I have a way of nicely generalising.

bryangingechen
bryangingechen previously approved these changes Apr 10, 2021
View reviewed changes
src/order/extension.lean Outdated Show resolved Hide resolved
@b-mehta
Copy link
Collaborator Author

b-mehta commented Apr 13, 2021

Okay I think the generalisation I was trying doesn't make anything easier - so I've effectively reverted.

@b-mehta b-mehta added awaiting-review The author would like community review of the PR and removed WIP Work in progress labels Apr 13, 2021
eric-wieser
eric-wieser reviewed Apr 20, 2021
View reviewed changes
src/order/zorn.lean Outdated Show resolved Hide resolved
@b-mehta @eric-wieser
Update src/order/zorn.lean
d0f14e1 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@semorrison
Copy link
Collaborator

bors merge

@github-actions github-actions bot 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 Apr 25, 2021
bors bot pushed a commit that referenced this pull request Apr 25, 2021
@b-mehta
feat(order/extension): extend partial order to linear order (#7142)
d052c52 
Adds a construction to extend a partial order to a linear order. Also fills in a missing Zorn variant.
@bors
Copy link

bors bot commented Apr 25, 2021

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(order/extension): extend partial order to linear order [Merged by Bors] - feat(order/extension): extend partial order to linear order Apr 25, 2021
@bors bors bot closed this Apr 25, 2021
@bors bors bot deleted the linear-extension branch April 25, 2021 10:07
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

@bryangingechen bryangingechen Awaiting requested review from bryangingechen

Assignees
No one assigned
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
4 participants
@b-mehta @semorrison @eric-wieser @bryangingechen