Data.Maybe.Lower

Definitions

data Lower : (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 (assoc-) snoc-lists, indexed by a `Maybe key`, where
  the empty list has a `Nothing` index.

Totality: total
Visibility: public export
Constructors:

LNothing : Lower lt Nothing (Just v)

LJust : lt v w -> Lower lt (Just v) (Just w)

Hints:

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

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

Uninhabited (Lower lt m Nothing)

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

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

Totality: total
Visibility: public export

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

  Implementation and alias for `trichotomy`.

Totality: total
Visibility: export