Bounded Class

Stream: Is there code for X?

[Alexandre Rademaker]

Do we have something similar to the Bounded Class from Haskell?

The context is the implementation of Bucketsort, where we would like to be able to construct the list [minBound .. maxBound ] from a given type a.

[Jireh Loreaux]

docs#BoundedOrder

[Jireh Loreaux]

Maybe + docs#LocallyFiniteOrder

[Jireh Loreaux]

Then you should be able to write Finset.Icc ⊥ ⊤ : Finset α for your type α.

[Eric Wieser]

That's just Finset.univ, surely?

[Jireh Loreaux]

yes, but I was thinking the point was to get Enum like features from Haskell, which is why I suggested LocallyFiniteOrder.

[Jireh Loreaux]

(but yes, Finset.Icc ⊥ ⊤ = Finset.univ for sure.)

[Alexandre Rademaker]

Hum. I found the classes you mentioned @Jireh Loreaux but it is not clear how to make an instance : BoundedOrder Char.

[Aaron Liu]

import Mathlib

instance : BoundedOrder Char where
  top := ⟨1114111, by decide⟩
  bot := ⟨0, by decide⟩
  le_top x := x.valid.by_cases
    (fun h => (h.trans (by decide)).le)
    (fun h => Nat.le_of_lt_add_one h.right)
  bot_le x := Nat.zero_le x.val.toNat

[Aaron Liu]

You can also just provide instances for Top Char and Bot Char and then not need to provide the proofs

[Alexandre Rademaker]

Thank you @Aaron Liu , I will try to connect with the @Jireh Loreaux suggestion now.