max_default/min_default

Stream: mathlib4

[Ruben Van de Velde]

It looks like docs#max_default / docs#min_default don't exist in lean4 - where should they go?

[Yaël Dillies]

I think we want to drop them entirely

[Yaël Dillies]

My plan is to make linear_order extend lattice. That wasn't possible in Lean 3 because linear_order was in core.

[Yaël Dillies]

Would people be happy with me carrying such a refactor even though it could technically wait for after the port?

[Eric Wieser]

Refactoring mathlib4 mid-port feels like a bad idea

[Scott Morrison]

I think this ship may have sailed, and it's going to be 6 months before we can do this refactor now...

[Scott Morrison]

@Ruben Van de Velde, you can add them to Mathlib/Init/Algebra/Order.lean.

[Yaël Dillies]

There's also the much more conservative option of copying all fields of lattice over to linear_order without actually extending it. That will only matter for instances of linear_order, and almost none of them references max_default/min_default anyway.