-
Notifications
You must be signed in to change notification settings - Fork 1k
[Merged by Bors] - refactor: move CategoryTheory.Category.Grpd to CategoryTheory.Groupoid.Grpd.Basic
#32735
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.
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
Conversation
PR summary e640e39324Import changes for modified filesNo significant changes to the import graph Import changes for all files
Declarations diffNo declarations were harmed in the making of this PR! 🐙 You can run this locally as follows## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>
## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>The doc-module for No changes to technical debt.You can run this locally as
note: file |
|
@dagurtomas Thank you for the suggestions. Here is the first PR just moving the |
|
This pull request has conflicts, please merge |
|
Thanks! bors merge |
|
Pull request successfully merged into master. Build succeeded: |
CategoryTheory.Category.Grpd to CategoryTheory.Groupoid.Grpd.BasicCategoryTheory.Category.Grpd to CategoryTheory.Groupoid.Grpd.Basic
…poid.Grpd.Basic` (leanprover-community#32735) Step one of several PRs, stemming from leanprover-community#29283 Co-authored-by: jlh18 <josephhua73@yahoo.com>
…poid.Grpd.Basic` (leanprover-community#32735) Step one of several PRs, stemming from leanprover-community#29283 Co-authored-by: jlh18 <josephhua73@yahoo.com>
Step one of several PRs, stemming from #29283