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: port changes to order/game_add #2532

Closed
wants to merge 14 commits into from
Closed

[Merged by Bors] - feat: port changes to order/game_add #2532

wants to merge 14 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Feb 28, 2023 •
edited by eric-wieser

Simultaneously ports various PRs on this file.

This also fixes a mis-ported alias in Mathlib/Order/RelIso/Basic.lean

Open in Gitpod

@vihdzp vihdzp added WIP Work in progress mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Feb 28, 2023
@vihdzp vihdzp mentioned this pull request Feb 28, 2023
Closed
1 task
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Feb 28, 2023
@vihdzp
feat(order/game_add): sym2.game_add (#18287)
7b1d4ab 
We define `sym2.game_add`, which is a relation `sym2 α → sym2 α → Prop` which expresses that one pair may be obtained from the other by decreasing either entry. We add a basic API, and prove well-foundedness.

Pair: leanprover-community/mathlib4#2532
This was referenced Mar 1, 2023
Closed
Closed
@vihdzp vihdzp removed the WIP Work in progress label Mar 1, 2023
@vihdzp vihdzp marked this pull request as ready for review March 1, 2023 11:11
@vihdzp vihdzp changed the title feat: port sym2.game_add feat: port changes to order/game_add Mar 1, 2023
bors bot pushed a commit to leanprover-community/mathlib that referenced this pull request Mar 1, 2023
@vihdzp
doc(order/game_add): minor doc improvement (#18525)
fee218f 
Ported along with other changes to the file: leanprover-community/mathlib4#2532
@eric-wieser
Copy link
Member

Can you update the SHAs to reflect which commits you ported? You can use https://leanprover-community.github.io/mathlib-port-status/file/order/game_add to help.

@eric-wieser eric-wieser added the awaiting-author A reviewer has asked the author a question or requested changes label Mar 18, 2023
@Parcly-Taxel Parcly-Taxel added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes needs-mathlib-SHA labels Mar 18, 2023
@semorrison semorrison added awaiting-author A reviewer has asked the author a question or requested changes and removed awaiting-review The author would like community review of the PR labels Mar 26, 2023
@Parcly-Taxel Parcly-Taxel added awaiting-review The author would like community review of the PR and removed awaiting-author A reviewer has asked the author a question or requested changes labels Mar 27, 2023
@semorrison semorrison added blocked-by-other-PR This PR depends on another PR which is still in the queue. and removed blocked-by-other-PR This PR depends on another PR which is still in the queue. labels Mar 27, 2023
vihdzp and others added 2 commits March 27, 2023 11:06
@vihdzp @eric-wieser
Update Mathlib/Order/GameAdd.lean
3440ca7 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@Parcly-Taxel
+Prod.
499a094
@Parcly-Taxel @eric-wieser
Update Mathlib/Order/GameAdd.lean
40f4fc1 
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
@semorrison
Copy link
Contributor

Can we please have the links to the port status dashboard, to make it easier to review the mathlib3 changes?

@Parcly-Taxel
Copy link
Collaborator

Can we please have the links to the port status dashboard, to make it easier to review the mathlib3 changes?

✅

@eric-wieser
Copy link
Member

eric-wieser commented Mar 27, 2023 •
edited

Can we please have the links to the port status dashboard, to make it easier to review the mathlib3 changes?

Arguably it's better not to have these; my intent was for the CI run to generate these links for you, which also means you don't have to trust the author actually pasted the right links.

Unfortunately that CI script seems to be a bit buggy right now, and it would probably be better if it actually made a real PR comment rather than annotations (which are limited to 10 and aren't hyperlinked) and a CI log (which no one knows to look for)

@eric-wieser
Copy link
Member

bors merge

Thanks!

@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 Mar 27, 2023
bors bot pushed a commit that referenced this pull request Mar 27, 2023
@vihdzp @Parcly-Taxel
feat: port changes to order/game_add (#2532)
426aed3 
Simultaneously ports various PRs on this file.

This also fixes a mis-ported alias in `Mathlib/Order/RelIso/Basic.lean`



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link

bors bot commented Mar 28, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port changes to order/game_add [Merged by Bors] - feat: port changes to order/game_add Mar 28, 2023
@bors bors bot closed this Mar 28, 2023
@bors bors bot deleted the sym2_game_add branch March 28, 2023 01:12
joelriou pushed a commit that referenced this pull request Mar 30, 2023
@vihdzp @Parcly-Taxel @joelriou
feat: port changes to order/game_add (#2532)
67d4b43 
Simultaneously ports various PRs on this file.

This also fixes a mis-ported alias in `Mathlib/Order/RelIso/Basic.lean`



Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@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 approved these changes

@Parcly-Taxel Parcly-Taxel Parcly-Taxel left review comments

Assignees
No one assigned
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
No open projects
Forward ports of mathlib3
Status: Awaiting mathport output
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@vihdzp @eric-wieser @semorrison @Parcly-Taxel