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
[Merged by Bors] - chore(combinatorics/quiver/path): reduce imports #17216
Conversation
Looks fine, but is |
I don't understand your comment. How does |
It's the first file in category theory that imports |
@YaelDillies The path category is for a pretty basic construction https://en.m.wikipedia.org/wiki/Free_category |
I'm so confused, and tbh a little annoyed at this conversation wasting time. It seems obvious that Please see https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Porting.20category.20theory/near/306557065 for the discussion that prompted this PR. It includes a PDF of the import hierarchy after this PR. Before this PR it also included the entire |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks!
bors r+
By using some lower-tech theorems, we can avoid importing the entire `algebra.order` hierarchy, significantly reducing the import dependencies of the basic category theory library. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Build failed: |
This graph would have been helpful to include in the PR description in the first place 😄 |
bors d+ |
✌️ semorrison can now approve this pull request. To approve and merge a pull request, simply reply with |
bors merge |
By using some lower-tech theorems, we can avoid importing the entire `algebra.order` hierarchy, significantly reducing the import dependencies of the basic category theory library. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
This PR was included in a batch that was canceled, it will be automatically retried |
By using some lower-tech theorems, we can avoid importing the entire `algebra.order` hierarchy, significantly reducing the import dependencies of the basic category theory library. Co-authored-by: Scott Morrison <scott.morrison@gmail.com>
Pull request successfully merged into master. Build succeeded: |
By using some lower-tech theorems, we can avoid importing the entire
algebra.order
hierarchy, significantly reducing the import dependencies of the basic category theory library.