Skip to content

[Merged by Bors] - feat: Small sets of games/surreals are bounded#10458

Closed
YaelDillies wants to merge 31 commits intomasterfrom
forward_ports
Closed

[Merged by Bors] - feat: Small sets of games/surreals are bounded#10458
YaelDillies wants to merge 31 commits intomasterfrom
forward_ports

Conversation

@YaelDillies
Copy link
Copy Markdown
Contributor

@YaelDillies YaelDillies commented Feb 12, 2024 •
edited by timotree3
Loading

Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in PGame.lean.

We don't port upper_bound_numeric (or lower_bound_numeric) because upper_bound was deleted following review feedback on the previous forward-porting PR #10566.

Open in Gitpod

@YaelDillies YaelDillies added awaiting-review mathlib3-pair This PR is a forward-port of a mathlib3 PR or part of one, either under review or recently merged labels Feb 12, 2024
@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Feb 12, 2024

I think we should regenerate that page one last time, if these really are the final forward ports

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 12, 2024

That would be great but I don't know how to do that.

Ruben-VandeVelde
Ruben-VandeVelde reviewed Feb 13, 2024
View reviewed changes
urkud
urkud reviewed Feb 14, 2024
View reviewed changes
urkud
urkud reviewed Feb 14, 2024
View reviewed changes
urkud
urkud reviewed Feb 14, 2024
View reviewed changes
@urkud
Copy link
Copy Markdown
Member

urkud commented Feb 14, 2024

Could you please split it into smaller PRs, each for 1 topic?

@urkud urkud added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Feb 14, 2024
@urkud urkud self-assigned this Feb 14, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Feb 14, 2024

It's a bit of a pain to split, so I'll only do it if you have a specific thing you would like to see in another PR.

@YaelDillies YaelDillies added awaiting-review and removed awaiting-author A reviewer has asked the author a question or requested changes. labels Feb 14, 2024
urkud
urkud reviewed Feb 14, 2024
View reviewed changes
urkud
urkud reviewed Feb 14, 2024
View reviewed changes
YaelDillies and others added 2 commits February 14, 2024 16:09
@YaelDillies @urkud
golf
1f7f6a2 
Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
@YaelDillies
reuse variables
9501869
@timotree3 timotree3 added awaiting-review and removed delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). labels Mar 3, 2024
eric-wieser
eric-wieser approved these changes Mar 8, 2024
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.

bors merge

Thanks!

@ghost ghost added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Mar 8, 2024
mathlib-bors bot pushed a commit that referenced this pull request Mar 8, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
776be0d 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 8, 2024

Build failed:

@eric-wieser
Copy link
Copy Markdown
Member

eric-wieser commented Mar 8, 2024

bors r-

bors d+

Looks like an easy fix.

@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 8, 2024

✌️ YaelDillies 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 This pull request has been delegated to the PR author (or occasionally another non-maintainer). label Mar 8, 2024
@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Mar 9, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 9, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
96ef680 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 9, 2024

Build failed:

@YaelDillies
Copy link
Copy Markdown
Contributor Author

YaelDillies commented Mar 9, 2024

bors merge

mathlib-bors bot pushed a commit that referenced this pull request Mar 9, 2024
@YaelDillies @urkud @timotree3
feat: Small sets of games/surreals are bounded (#10458)
d004cbb 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
@mathlib-bors
Copy link
Copy Markdown
Contributor

mathlib-bors bot commented Mar 9, 2024

Pull request successfully merged into master.

Build succeeded:

@mathlib-bors mathlib-bors bot changed the title feat: Small sets of games/surreals are bounded [Merged by Bors] - feat: Small sets of games/surreals are bounded Mar 9, 2024
@mathlib-bors mathlib-bors bot closed this Mar 9, 2024
@mathlib-bors mathlib-bors bot deleted the forward_ports branch March 9, 2024 22:56
kbuzzard pushed a commit that referenced this pull request Mar 12, 2024
@YaelDillies @urkud
@timotree3 @kbuzzard
feat: Small sets of games/surreals are bounded (#10458)
0e9d003 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
dagurtomas pushed a commit that referenced this pull request Mar 22, 2024
@YaelDillies @urkud
@timotree3 @dagurtomas
feat: Small sets of games/surreals are bounded (#10458)
2129ca0 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
utensil pushed a commit that referenced this pull request Mar 26, 2024
@YaelDillies @urkud
@timotree3 @utensil
feat: Small sets of games/surreals are bounded (#10458)
9493f20 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
xgenereux pushed a commit that referenced this pull request Apr 15, 2024
@YaelDillies @urkud
@timotree3 @xgenereux
feat: Small sets of games/surreals are bounded (#10458)
b72118a 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
uniwuni pushed a commit that referenced this pull request Apr 19, 2024
@YaelDillies @urkud
@timotree3 @uniwuni
feat: Small sets of games/surreals are bounded (#10458)
347c5b0 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
callesonne pushed a commit that referenced this pull request Apr 22, 2024
@YaelDillies @urkud
@timotree3 @callesonne
feat: Small sets of games/surreals are bounded (#10458)
e6c8970 
Finish forwarding porting leanprover-community/mathlib3#15260 after #10566 ported just the changes in `PGame.lean`.

We don't port `upper_bound_numeric` (or `lower_bound_numeric`) because `upper_bound` was deleted following review feedback on the previous forward-porting PR #10566.



Co-authored-by: Yury G. Kudryashov <urkud@urkud.name>
Co-authored-by: timotree3 <timorcb@gmail.com>
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

@Ruben-VandeVelde Ruben-VandeVelde Ruben-VandeVelde left review comments

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

+1 more reviewer

@timotree3 timotree3 timotree3 approved these changes

Reviewers whose approvals may not affect merge requirements

Assignees

@urkud urkud

@eric-wieser eric-wieser

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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. t-logic Logic (model theory, etc)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

5 participants

@YaelDillies @eric-wieser @urkud @timotree3 @Ruben-VandeVelde