Skip to content

[Merged by Bors] - feat: port Topology.Category.Top.Limits.Basic#3487

Closed
mattrobball wants to merge 36 commits intomasterfrom
port/Topology.Category.Top.Limits
Closed

[Merged by Bors] - feat: port Topology.Category.Top.Limits.Basic#3487
mattrobball wants to merge 36 commits intomasterfrom
port/Topology.Category.Top.Limits

Conversation

@mattrobball
Copy link
Copy Markdown
Contributor

@mattrobball mattrobball commented Apr 17, 2023 •
edited by Parcly-Taxel
Loading

@mattrobball mattrobball added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 17, 2023
@mattrobball mattrobball added the help-wanted The author needs attention to resolve issues label Apr 25, 2023
@kim-em kim-em added the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 26, 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 Apr 27, 2023
@Parcly-Taxel Parcly-Taxel removed the blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) label Apr 27, 2023
@Parcly-Taxel Parcly-Taxel changed the title feat: port Topology.Category.Top.Limits feat: port Topology.Category.Top.Limits.Basic Apr 27, 2023
@Parcly-Taxel Parcly-Taxel removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Apr 27, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 27, 2023

This PR/issue depends on:

@Parcly-Taxel Parcly-Taxel removed the WIP Work in progress label Apr 27, 2023
@Parcly-Taxel
Copy link
Copy Markdown
Collaborator

Parcly-Taxel commented Apr 27, 2023 •
edited
Loading

Please check if putting nolint on the TopCatMax is the right decision here.

@Parcly-Taxel Parcly-Taxel added awaiting-review help-wanted The author needs attention to resolve issues and removed help-wanted The author needs attention to resolve issues labels Apr 27, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 27, 2023

bors merge

@github-actions github-actions bot added ready-to-merge This PR has been sent to bors. and removed awaiting-review labels Apr 27, 2023
@Parcly-Taxel Parcly-Taxel removed the help-wanted The author needs attention to resolve issues label Apr 27, 2023
bors bot pushed a commit that referenced this pull request Apr 27, 2023
@mattrobball @kim-em
@Parcly-Taxel @adamtopaz
feat: port Topology.Category.Top.Limits.Basic (#3487)
1c05ad4 
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 27, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port Topology.Category.Top.Limits.Basic [Merged by Bors] - feat: port Topology.Category.Top.Limits.Basic Apr 27, 2023
@bors bors bot closed this Apr 27, 2023
@bors bors bot deleted the port/Topology.Category.Top.Limits branch April 27, 2023 15:21
mattrobball added a commit that referenced this pull request Apr 28, 2023
@mattrobball
restore changes from #3487
59fdc41
@mattrobball mattrobball mentioned this pull request Apr 28, 2023
Closed
mattrobball added a commit that referenced this pull request May 5, 2023
@mattrobball
restore changes from #3487
629a95c
kim-em added a commit that referenced this pull request May 10, 2023
@mattrobball @kim-em
@Parcly-Taxel @adamtopaz
feat: port Topology.Category.Top.Limits.Basic (#3487)
129f0cd 
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
hrmacbeth pushed a commit that referenced this pull request May 10, 2023
@mattrobball @kim-em
@Parcly-Taxel @adamtopaz @hrmacbeth
feat: port Topology.Category.Top.Limits.Basic (#3487)
89f59fd 
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
hrmacbeth pushed a commit that referenced this pull request May 11, 2023
@mattrobball @kim-em
@Parcly-Taxel @adamtopaz @hrmacbeth
feat: port Topology.Category.Top.Limits.Basic (#3487)
997c3d0 
Co-authored-by: Scott Morrison <scott@tqft.net>
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
Co-authored-by: Parcly Taxel <reddeloostw@gmail.com>
Co-authored-by: adamtopaz <github@adamtopaz.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

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

@mattrobball @kim-em @Parcly-Taxel @adamtopaz