Skip to content

[Merged by Bors] - feat: meta code for the category_theory port#755

Closed
kim-em wants to merge 5 commits intomasterfrom
category_theory_meta
Closed

[Merged by Bors] - feat: meta code for the category_theory port#755
kim-em wants to merge 5 commits intomasterfrom
category_theory_meta

Conversation

@kim-em
Copy link
Copy Markdown
Contributor

@kim-em kim-em commented Nov 27, 2022 •
edited by bors bot
Loading

No description provided.

@kim-em kim-em mentioned this pull request Nov 27, 2022
Closed
1 task
kim-em
kim-em commented Nov 28, 2022
View reviewed changes
kim-em
kim-em commented Nov 28, 2022
View reviewed changes
@kim-em kim-em requested a review from digama0 November 28, 2022 01:29
@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 Nov 28, 2022
@kim-em kim-em removed the merge-conflict The PR has a merge conflict with master, and needs manual merging. (this label is managed by a bot) label Nov 28, 2022
fpvandoorn
fpvandoorn approved these changes Nov 30, 2022
View reviewed changes
Copy link
Copy Markdown
Member

@fpvandoorn fpvandoorn left a comment

Choose a reason for hiding this comment

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

bors d+

@bors
Copy link
Copy Markdown

bors bot commented Nov 30, 2022

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

@kim-em kim-em added delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). and removed awaiting-review labels Nov 30, 2022
kim-em
kim-em commented Nov 30, 2022
View reviewed changes
@kim-em @fpvandoorn
Apply suggestions from code review
a3bfa6e 
Co-authored-by: Floris van Doorn <fpvdoorn@gmail.com>
@kim-em
Copy link
Copy Markdown
Contributor Author

kim-em commented Nov 30, 2022

bors merge

@github-actions github-actions bot added the ready-to-merge This PR has been sent to bors. label Nov 30, 2022
bors bot pushed a commit that referenced this pull request Nov 30, 2022
@kim-em
feat: meta code for the category_theory port (#755)
dc615a3 
Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
@bors
Copy link
Copy Markdown

bors bot commented Nov 30, 2022

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: meta code for the category_theory port [Merged by Bors] - feat: meta code for the category_theory port Nov 30, 2022
@bors bors bot closed this Nov 30, 2022
@bors bors bot deleted the category_theory_meta branch November 30, 2022 16:54
bors bot pushed a commit that referenced this pull request Dec 1, 2022
@kim-em
port: several files from category_theory (#749)
c5ffca6 
mathlib git sha: 8350c34a64b9bc3fc64335df8006bffcadc7baa6

Also ports the reassoc attribute.

- [x] depends on: #755 

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@fpvandoorn fpvandoorn fpvandoorn approved these changes

@digama0 digama0 Awaiting requested review from digama0

Assignees

No one assigned

Labels

delegated This pull request has been delegated to the PR author (or occasionally another non-maintainer). 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.

2 participants

@kim-em @fpvandoorn