Deprecated instances about order structures. #
@[deprecated "This was a leftover from Lean 3, and has not been needed." (since := "2024-11-26")]
instance
isStrictTotalOrder_of_linearOrder
{α : Type u_1}
[LinearOrder α]
:
IsStrictTotalOrder α fun (x1 x2 : α) => x1 < x2