Data.Maybe.NothingMin

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 minimal value.
  
  This is useful, for instance, when implementing provably
  sorted snoc-lists, indexed by a `Maybe key`, where
  the empty snoc-list has a `Nothing` index:
  
  ```idris example
  data AssocSnocList : (ix : Maybe Bits8) -> (a : Type) -> Type where
    Lin  : AssocSnocList Nothing a
    (:<) :  (ps : AssocSnocList ix a)
         -> (p : (Bits8, a))
         -> (0 prf : LT (<) ix (Just $ fst p))
         => AssocSnocList (Just $ fst p) a
  ```

Totality: total
Visibility: public export
Constructors:

LTNothing : LT lt Nothing (Just v)

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

Hints:

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

Uninhabited (LT lt m Nothing)

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