Data.Maybe.Upper

Definitions

data Upper : (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 : Upper (<) (Just $ fst p) ix)
         => AssocList (Just $ fst p) a
  ```

Totality: total
Visibility: public export
Constructors:

UNothing : Upper lt (Just v) Nothing

UJust : lt v w -> Upper lt (Just v) (Just w)

Hints:

Transitive a lt => Transitive (Maybe a) (Upper lt)

Trichotomous a lt => Trichotomous (Maybe a) (Upper lt)

Uninhabited (Upper lt Nothing m)

Strict a lt => Uninhabited (Upper lt (Just k) (Just k))

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

Totality: total
Visibility: public export

comp : Trichotomous a lt => (m1 : Maybe a) -> (m2 : Maybe a) -> Trichotomy (Upper lt) m1 m2

  Implementation and alias for `trichotomy`.

Totality: total
Visibility: export