Commit 2022-01-12 17:52 258686f9

fix(order/complete_lattice): fix diamond in sup vs max and min vs inf (#11309) complete_linear_order has separate max and sup fields. There is no need to have both, so this removes one of them by telling the structure compiler to merge the two fields. The same is true of inf and min. As well as diamonds being possible in the abstract case, a handful of concrete example of this diamond existed. linear_order instances with default-populated fields were usually to blame.