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

[Merged by Bors] - feat(*): update to Lean 3.49#17470

Closed
kim-em wants to merge 10 commits intomasterfrom
backport_min_max
Closed

[Merged by Bors] - feat(*): update to Lean 3.49#17470
kim-em wants to merge 10 commits intomasterfrom
backport_min_max

Conversation

@kim-em
Copy link
Copy Markdown
Collaborator

@kim-em kim-em commented Nov 11, 2022 •
edited
Loading

In leanprover-community/lean#779 we backported the Lean 4 definition of min and max in linear_order.

Open in Gitpod

@kim-em kim-em added the WIP Work in progress label Nov 11, 2022
This was referenced Nov 11, 2022
Closed
Closed
@gebner
Copy link
Copy Markdown
Member

gebner commented Nov 11, 2022

Lean 3.49 is out with the min/max backport.

@gebner gebner added the awaiting-author A reviewer has asked the author a question or requested changes label Nov 11, 2022
@gebner gebner mentioned this pull request Nov 11, 2022
Closed
@kim-em kim-em changed the title feat(order/*): backport Lean 4 definitions of min and max feat(*): update to Lean 3.49 Nov 12, 2022
@kim-em kim-em requested a review from a team as a code owner November 12, 2022 06:20
@bryangingechen bryangingechen linked an issue Nov 12, 2022 that may be closed by this pull request
Lean 3.49.0 compatibility #17486
Closed
@kim-em kim-em requested a review from a team as a code owner November 12, 2022 21:55
@kim-em kim-em added awaiting-CI The author would like to see what CI has to say before doing more work. awaiting-review The author would like community review of the PR and removed WIP Work in progress awaiting-author A reviewer has asked the author a question or requested changes labels Nov 12, 2022
eric-wieser
eric-wieser approved these changes Nov 12, 2022
View reviewed changes
Copy link
Copy Markdown
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.

Looks reasonable, will let someone who's not on mobile take a final look

@eric-wieser eric-wieser added the t-order Order hierarchy label Nov 12, 2022
bryangingechen
bryangingechen approved these changes Nov 12, 2022
View reviewed changes
Copy link
Copy Markdown
Collaborator

@bryangingechen bryangingechen 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 r+

@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 Nov 12, 2022
@bors
Copy link
Copy Markdown

bors bot commented Nov 12, 2022

👎 Rejected by label

@bryangingechen
Copy link
Copy Markdown
Collaborator

bryangingechen commented Nov 12, 2022

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 12, 2022

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

@github-actions github-actions bot added the delegated The PR author may merge after reviewing final suggestions. label Nov 12, 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 Nov 13, 2022
@kim-em
Copy link
Copy Markdown
Collaborator Author

kim-em commented Nov 13, 2022

bors merge

bors bot pushed a commit that referenced this pull request Nov 13, 2022
@kim-em
feat(*): update to Lean 3.49 (#17470)
82a5373 
In leanprover-community/lean#779 we backported the Lean 4 definition of min and max in `linear_order`.



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

bors bot commented Nov 13, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat(*): update to Lean 3.49 [Merged by Bors] - feat(*): update to Lean 3.49 Nov 13, 2022
@bors bors bot closed this Nov 13, 2022
@bors bors bot deleted the backport_min_max branch November 13, 2022 09:22
Sign up for free to subscribe to this conversation on GitHub. Already have an account? Sign in.

Reviewers

2 more reviewers

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

@bryangingechen bryangingechen bryangingechen approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

No one assigned

Labels

delegated The PR author may merge after reviewing final suggestions. ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) t-order Order hierarchy

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

Lean 3.49.0 compatibility

5 participants

@kim-em @gebner @bryangingechen @eric-wieser @leanprover-community-bot-assistant