Skip to content

[Merged by Bors] - feat Port/data.list.big operators.lemmas#1423

Closed
casavaca wants to merge 9 commits intomasterfrom
port/Data.List.BigOperators.Lemmas
Closed

[Merged by Bors] - feat Port/data.list.big operators.lemmas#1423
casavaca wants to merge 9 commits intomasterfrom
port/Data.List.BigOperators.Lemmas

Conversation

@casavaca
Copy link
Copy Markdown
Contributor

@casavaca casavaca commented Jan 8, 2023 •
edited by jcommelin
Loading

@casavaca casavaca added WIP Work in progress blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Jan 8, 2023
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 8, 2023
@casavaca
Copy link
Copy Markdown
Contributor Author

casavaca commented Jan 8, 2023

Should work after #1380 is merged.

@casavaca casavaca added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) awaiting-review mathlib-port This is a port of a theory file from mathlib. and removed WIP Work in progress labels Jan 8, 2023
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 8, 2023
@casavaca casavaca changed the title Port/data.list.big operators.lemmas feat Port/data.list.big operators.lemmas Jan 8, 2023
@casavaca
Copy link
Copy Markdown
Contributor Author

casavaca commented Jan 8, 2023

@semorrison why the label blocked-by-other-PR is removed?

@ChrisHughes24 ChrisHughes24 added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 9, 2023
@kim-em kim-em removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Jan 9, 2023
@kim-em kim-em added the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 10, 2023
@casavaca casavaca force-pushed the port/Data.List.BigOperators.Lemmas branch from ea07ddf to 4582ab0 Compare January 10, 2023 08:02
@casavaca casavaca removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Jan 10, 2023
jcommelin
jcommelin reviewed Jan 10, 2023
View reviewed changes
@jcommelin jcommelin added awaiting-author A reviewer has asked the author a question or requested changes. and removed awaiting-review labels Jan 10, 2023
ChrisHughes24 and others added 3 commits January 10, 2023 12:14
@ChrisHughes24 @jcommelin
Apply suggestions from code review
5a6b2c1 
Co-authored-by: Johan Commelin <johan@commelin.net>
@ChrisHughes24
fix typo
f18be36
@ChrisHughes24
fix build
dcc4b1e
jcommelin
jcommelin approved these changes Jan 10, 2023
View reviewed changes
Copy link
Copy Markdown
Member

@jcommelin jcommelin 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 merge

@kim-em kim-em added the ready-to-merge This PR has been sent to bors. label Jan 10, 2023
@kim-em kim-em removed the awaiting-author A reviewer has asked the author a question or requested changes. label Jan 10, 2023
bors bot pushed a commit that referenced this pull request Jan 10, 2023
@casavaca @ChrisHughes24
feat Port/data.list.big operators.lemmas (#1423)
f6f04c9 
- [x] depends on #1380 

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Jan 10, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat Port/data.list.big operators.lemmas [Merged by Bors] - feat Port/data.list.big operators.lemmas Jan 10, 2023
@bors bors bot closed this Jan 10, 2023
@bors bors bot deleted the port/Data.List.BigOperators.Lemmas branch January 10, 2023 12:36
jcommelin pushed a commit that referenced this pull request Jan 23, 2023
@casavaca @ChrisHughes24 @jcommelin
feat Port/data.list.big operators.lemmas (#1423)
ac0e1ef 
- [x] depends on #1380 

Co-authored-by: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>
Co-authored-by: ChrisHughes24 <chrishughes24@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@jcommelin jcommelin jcommelin approved these changes

Assignees

No one assigned

Labels

mathlib-port This is a port of a theory file from mathlib. ready-to-merge This PR has been sent to bors.

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

4 participants

@casavaca @jcommelin @kim-em @ChrisHughes24