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(order/game_add): move game_add to its own file #15885

Closed
wants to merge 18 commits into from
Closed

[Merged by Bors] - refactor(order/game_add): move game_add to its own file #15885

wants to merge 18 commits into from

Conversation

vihdzp
Copy link
Collaborator

@vihdzp vihdzp commented Aug 5, 2022 •
edited by github-actions bot

We move game_add from the logic/hydra file to a new order/game_add file, and move it in the prod namespace in preparation for a future PR that will add sym2.game_add.

Open in Gitpod

@vihdzp vihdzp added the awaiting-review The author would like community review of the PR label Aug 5, 2022
@vihdzp vihdzp requested a review from alreadydone August 5, 2022 22:56
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 5, 2022
@alreadydone
Copy link
Collaborator

Looks good but I don't think it needs to depend on #15884?

@vihdzp
Copy link
Collaborator Author

vihdzp commented Aug 6, 2022

It does for the ≤ notation on subrelations to work. I could just have stronger imports, but I hope that other PR won't take long to be merged.

@vihdzp vihdzp mentioned this pull request Aug 7, 2022
Closed
@mathlib-dependent-issues-bot mathlib-dependent-issues-bot removed the blocked-by-other-PR This PR depends on another PR which is still in the queue. A bot manages this label via PR comment. label Aug 8, 2022
@mathlib-dependent-issues-bot
Copy link
Collaborator

This PR/issue depends on:

alreadydone
alreadydone approved these changes Aug 10, 2022
View reviewed changes
Copy link
Collaborator

@alreadydone alreadydone left a comment

Choose a reason for hiding this comment

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

Thanks, looks good!

urkud
urkud reviewed Aug 15, 2022
View reviewed changes
src/order/game_add.lean Outdated Show resolved Hide resolved
@bors
Copy link

bors bot commented Aug 15, 2022

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

@vihdzp
Copy link
Collaborator Author

vihdzp commented Aug 16, 2022

bors r+

@bors
Copy link

bors bot commented Aug 16, 2022

Canceled.

@vihdzp
Copy link
Collaborator Author

vihdzp commented Aug 16, 2022

bors r+

bors bot pushed a commit that referenced this pull request Aug 16, 2022
@vihdzp
refactor(order/game_add): move game_add to its own file (#15885)
b7f327b 
We move `game_add` from the `logic/hydra` file to a new `order/game_add` file, and move it in the `prod` namespace in preparation for a future PR that will add `sym2.game_add`.
@bors
Copy link

bors bot commented Aug 16, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title refactor(order/game_add): move game_add to its own file [Merged by Bors] - refactor(order/game_add): move game_add to its own file Aug 16, 2022
@bors bors bot closed this Aug 16, 2022
@bors bors bot deleted the game_add_move branch August 16, 2022 13:24
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

@alreadydone alreadydone alreadydone approved these changes

Assignees
No one assigned
Labels
awaiting-review The author would like community review of the PR
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

None yet
4 participants
@vihdzp @alreadydone @mathlib-dependent-issues-bot @urkud