Skip to content

[Merged by Bors] - feat: Port CategoryTheory.Monad.Limits#3533

Closed
adamtopaz wants to merge 32 commits intomasterfrom
port/CategoryTheory.Monad.Limits
Closed

[Merged by Bors] - feat: Port CategoryTheory.Monad.Limits#3533
adamtopaz wants to merge 32 commits intomasterfrom
port/CategoryTheory.Monad.Limits

Conversation

@adamtopaz
Copy link
Copy Markdown
Contributor

@adamtopaz adamtopaz commented Apr 20, 2023 •
edited by github-actions bot
Loading

adamtopaz added 25 commits April 19, 2023 09:54
@adamtopaz
feat: port CategoryTheory.Monad.Adjunction
37f1b97
@adamtopaz
Initial file copy from mathport
d61ea4d
@adamtopaz
automated fixes
32b2ad4 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@adamtopaz
wip
29c1c9b
@adamtopaz
finish off modulo reassoc issue
bebdd1d
@adamtopaz
fix docstrings
69be70c
@adamtopaz
test
fd75480
@adamtopaz
lint
9624984
@adamtopaz
alphabetize
bef339e
@adamtopaz
fix
8644001
@adamtopaz
fix
d9cba10
@adamtopaz
fix
62fe569
@adamtopaz
shuffle files/imports
f1acf8c
@adamtopaz
remove simp
690b2cb
@adamtopaz
cleanup
7a78391
@adamtopaz
fix
4c7428f
@adamtopaz
fix
c7966d8
@adamtopaz
fix
a0fcda4
@adamtopaz
Merge branch 'reassoc_test' into port/CategoryTheory.Monad.Adjunction
89d64ef
@adamtopaz
fix
306ec40
@adamtopaz
feat: port CategoryTheory.Monad.Limits
30cb77f
@adamtopaz
Initial file copy from mathport
1b5da69
@adamtopaz
automated fixes
d8c9820 
Mathbin -> Mathlib
fix certain import statements
move "by" to end of line
add import to Mathlib.lean
@adamtopaz
Merge branch 'port/CategoryTheory.Monad.Adjunction' into port/Categor…
f8bfdd7 
…yTheory.Monad.Limits
@adamtopaz
wip
a1f33a8
@adamtopaz adamtopaz added WIP Work in progress mathlib-port This is a port of a theory file from mathlib. labels Apr 20, 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 20, 2023
@adamtopaz adamtopaz added awaiting-review and removed WIP Work in progress labels Apr 20, 2023
@Parcly-Taxel Parcly-Taxel added blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) and removed blocked-by-other-PR This PR depends on another PR (this label is automatically managed by a bot) labels Apr 20, 2023
@kim-em
Copy link
Copy Markdown
Contributor

kim-em commented Apr 20, 2023

This PR/issue depends on:

@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Apr 20, 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 20, 2023
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Merge conflict.

@ChrisHughes24
Copy link
Copy Markdown
Member

ChrisHughes24 commented Apr 20, 2023

bors merge

bors bot pushed a commit that referenced this pull request Apr 20, 2023
@adamtopaz @Parcly-Taxel
feat: Port CategoryTheory.Monad.Limits (#3533)
9d37e73 
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Apr 20, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: Port CategoryTheory.Monad.Limits [Merged by Bors] - feat: Port CategoryTheory.Monad.Limits Apr 20, 2023
@bors bors bot closed this Apr 20, 2023
@bors bors bot deleted the port/CategoryTheory.Monad.Limits branch April 20, 2023 18:48
kbuzzard pushed a commit that referenced this pull request Apr 22, 2023
@adamtopaz @Parcly-Taxel @kbuzzard
feat: Port CategoryTheory.Monad.Limits (#3533)
f4b1f95 
Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>
kim-em pushed a commit that referenced this pull request May 10, 2023
@adamtopaz @Parcly-Taxel
feat: Port CategoryTheory.Monad.Limits (#3533)
4b3f0cb 
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

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

@adamtopaz @kim-em @ChrisHughes24 @Parcly-Taxel