Data.Maybe.NothingMax

Definitions

data LT : (a -> a -> Type) -> Maybe a -> Maybe a -> Type

  A total order for `Maybe a` where `a` has a total order
  and `Nothing` is the maximal value.
  
  This is useful, for instance, when implementing provably
  sorted (assoc-) lists, indexed by a `Maybe key`, where
  the empty list has a `Nothing` index:
  
  ```idris example
  data AssocList : (ix : Maybe Bits8) -> (a : Type) -> Type where
    Nil  : AssocList Nothing a
    (::) :  (p : (Bits8, a))
         -> (ps : AssocList ix a)
         -> (0 prf : LT (<) (Just $ fst p) ix)
         => AssocList (Just $ fst p) a
  ```

Totality: total
Visibility: public export
Constructors:

LTNothing : LT lt (Just v) Nothing

LTJust : lt v w -> LT lt (Just v) (Just w)

Hints:

Total a lt => Total (Maybe a) (LT lt)

Uninhabited (LT lt Nothing m)

Total a lt => Uninhabited (LT lt (Just k) (Just k))

fromLT : LT lt (Just a) (Just b) -> lt a b

Totality: total
Visibility: public export

comp : Total a lt => (m1 : Maybe a) -> (m2 : Maybe a) -> Trichotomy (LT lt) m1 m2

  Implementation and alias for `trichotomy`.

Totality: total
Visibility: export