Moving order structures to mathlib

Stream: general

[Yaël Dillies]

Mario Carneiro said:

Oh, I just realized that one of the areas I was most looking forward to refactoring as a result of the move, the stuff on order structures, was not included as part of the big move. Have we looked at giving the same treatment to the preorder, partial_order, linear_order classes in core?

What's the plan now? Is it still in the realm of possibilities to move preorder, partial_order, linear_order to mathlib?

[Johan Commelin]

What are the cons and pros in your eyes?

[Yaël Dillies]

Pros:

• Better flexibility for the very beginning of the order hierarchy
• No need to have weird lists of "lemmas missing in core"

Cons:

• Unknown amount to be pulled out of core/duplicated before that happens. I was tricked by docgen into thinking we were close, so I opened lean#629 a while back.