Commit 2022-11-27 23:52 97be0de9
View on Github →chore(order/bounded_order): split (#17730)
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.