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(order/bounded_order): split #17730
Conversation
I've just noticed the mathlib4 PR leanprover-community/mathlib4#697 which ports all of this file, so my motivation to split it has now gone away. Edit: I've now noticed that the PR is WIP and only ports the first quarter of this file, so splitting is now again perhaps a good idea (perhaps an even better idea, because it means that we'll easily be able to port one of the four files completely now, rather than 1/4-porting a too-long file) |
bors merge p=10 |
The file `order.bounded_order` was over 2000 lines long and I wanted to port a small part of it in the middle so I've broken it into four files `order.bounded_order`, `order.with_bot`, `order.prop_instances` and `order.disjoint`. No lemmas should have been added or removed. Because `order.bounded_order` contains less than before I had to add a few more imports to other files.
bors merge |
1 similar comment
bors merge |
The file `order.bounded_order` was over 2000 lines long and I wanted to port a small part of it in the middle so I've broken it into four files `order.bounded_order`, `order.with_bot`, `order.prop_instances` and `order.disjoint`. No lemmas should have been added or removed. Because `order.bounded_order` contains less than before I had to add a few more imports to other files.
Pull request successfully merged into master. Build succeeded: |
- [x] depends on: #642 - [x] depends on: leanprover-community/mathlib#17730 Tracking mathlib commit: [e50b8c261b0a000b806ec0e1356b41945eda61f7](leanprover-community/mathlib@e50b8c2) Co-authored-by: David Wärn <codwarn@gmail.com> Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Scott Morrison <scott@tqft.net>
The file
order.bounded_order
was over 2000 lines long and I wanted to port a small part of it in the middle so I've broken it into four filesorder.bounded_order
,order.with_bot
,order.prop_instances
andorder.disjoint
. No lemmas should have been added or removed. Becauseorder.bounded_order
contains less than before I had to add a few more imports to other files.