Linear orders

Stream: new members

[Heather Macbeth]

I am trying to navigate the order library. How would I express that something is a linear_order and also has ⊤ and ⊥ elements? Do I use [linear_order ι] [bounded_lattice ι]? (I fear that I would be introducing an order twice by doing this.)

[Johan Commelin]

Yup... that wouldn't work :sad: It would be nice to have mixins here...

[Johan Commelin]

I guess complete_linear_order gives you more than you want, right?

[Heather Macbeth]

It's more than necessary. But it's fine for my purposes (closed intervals in the reals, ultimately). Thanks!

[Adam Topaz]

That's strange... Closed intervals form a linear order? Doesn't linear order require that any two things are comparable?

[Heather Macbeth]

The order on the points in a single closed interval.

[Adam Topaz]

Oh :)

[Yury G. Kudryashov]

If you're going to add a def for complete_linear_order (Icc a b) it should assume conditionally_complete_linear_order α. It can't be an instance because it also needs a ≤ b`.