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] - feat: port/CategoryTheory.Category.Cat #2375

Closed
wants to merge 11 commits into from
Closed

[Merged by Bors] - feat: port/CategoryTheory.Category.Cat #2375

wants to merge 11 commits into from

Conversation

mattrobball
Copy link
Collaborator

@mattrobball mattrobball commented Feb 19, 2023 •
edited by github-actions bot

@mattrobball
feat: port CategoryTheory.Category.Cat
967e14a
@mattrobball
Initial file copy from mathport
e14a0f5
@mattrobball
automated fixes
64556c5 
Mathbin -> Mathlib

fix certain import statements

move "by" to end of line

add import to Mathlib.lean
@mattrobball
Squashed commit of the following:
dfa581d 
commit 24c70cb
Merge: 38a89b8 18f8822
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:20:59 2023 -0500

    Merge remote-tracking branch 'refs/remotes/origin/port/CategoryTheory.DiscreteCategory' into port/CategoryTheory.DiscreteCategory

commit 38a89b8
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:20:24 2023 -0500

    lint some more

commit 18f8822
Merge: eb14644 68e722a
Author: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
Date:   Thu Feb 16 20:16:53 2023 -0500

    Merge branch 'master' into port/CategoryTheory.DiscreteCategory

commit eb14644
Author: Matthew Ballard <matt@mrb.email>
Date:   Thu Feb 16 20:14:21 2023 -0500

    lint

commit 8860e0d
Author: adamtopaz <github@adamtopaz.com>
Date:   Thu Feb 16 17:33:00 2023 -0700

    get file to build

commit 2203485
Author: adamtopaz <github@adamtopaz.com>
Date:   Tue Feb 14 22:06:54 2023 -0700

    automated fixes

    Mathbin -> Mathlib

    fix certain import statements

    move "by" to end of line

    add import to Mathlib.lean

commit 10bf4bb
Author: adamtopaz <github@adamtopaz.com>
Date:   Tue Feb 14 22:06:54 2023 -0700

    Initial file copy from mathport

commit 82e2512
Author: adamtopaz <github@adamtopaz.com>
Date:   Tue Feb 14 22:06:54 2023 -0700

    feat: port CategoryTheory.DiscreteCategory
@mattrobball
remove script
25b7383
@mattrobball
fix errors; lint
405cecc
@mattrobball mattrobball added the mathlib-port This is a port of a theory file from mathlib. label Feb 19, 2023
@semorrison semorrison added the blocked-by-math-PR This PR depends on another PR to Mathlib label Feb 19, 2023
@mattrobball mattrobball mentioned this pull request Feb 20, 2023
Closed
1 task
@semorrison semorrison removed the blocked-by-math-PR This PR depends on another PR to Mathlib label Feb 21, 2023
@semorrison
Copy link
Contributor

This PR/issue depends on:

@semorrison semorrison added the merge-conflict The PR has a merge conflict with master, and needs manual merging. label Feb 21, 2023
@mattrobball mattrobball added awaiting-review The author would like community review of the PR and removed merge-conflict The PR has a merge conflict with master, and needs manual merging. labels Feb 22, 2023
@dupuisf
Copy link
Contributor

dupuisf commented Feb 22, 2023 •
edited

There are two extra files (Mathlib.lean.orig and another .orig file) being added by mistake here.

@mattrobball
Copy link
Collaborator Author

There are two extra files (Mathlib.lean.orig and another .orig file) being added by mistake here.

Thanks. They are gone now.

jcommelin
jcommelin approved these changes Feb 22, 2023
View reviewed changes
Copy link
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

@semorrison semorrison added ready-to-merge This PR has been sent to bors. and removed awaiting-review The author would like community review of the PR labels Feb 22, 2023
bors bot pushed a commit that referenced this pull request Feb 22, 2023
@mattrobball
feat: port/CategoryTheory.Category.Cat (#2375)
f89a71d 
Co-authored-by: Matthew Robert Ballard <100034030+mattrobball@users.noreply.github.com>
@bors
Copy link

bors bot commented Feb 22, 2023

Pull request successfully merged into master.

Build succeeded:

@bors bors bot changed the title feat: port/CategoryTheory.Category.Cat [Merged by Bors] - feat: port/CategoryTheory.Category.Cat Feb 22, 2023
@bors bors bot closed this Feb 22, 2023
@bors bors bot deleted the port/CategoryTheory.Category.Cat branch February 22, 2023 03:28
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.

None yet
4 participants
@mattrobball @semorrison @dupuisf @jcommelin