## Stream: general

### Topic: with_top max/sup diamond

#### Yury G. Kudryashov (Oct 31 2020 at 04:53):

There are two versions of sup on with_top α if α is a linear order. One comes from docs#with_top.semilattice_sup and the other one comes from docs#lattice_of_linear_order and docs#with_top.linear_order. This is why, e.g., docs#ennreal.sup_eq_max is not a rfl. What should we do? Add max/min to the signature of linear_order with default values?

Last updated: May 13 2021 at 18:26 UTC