Data.Order

Additional data types related to ordering notions

Definitions

data Trichotomous : (a -> a -> Type) -> (a -> a -> Type) -> (a -> a -> Type) -> a -> a -> Type

  Trichotomous formalises the fact that three relations are mutually exclusive.
  It is meant to be used with relations that complement each other so that the
  `Trichotomous lt eq gt` relation is the total relation.

Totality: total
Visibility: public export
Constructors:

MkLT : lt v w -> Not (eq v w) -> Not (gt v w) -> Trichotomous lt eq gt v w

MkEQ : Not (lt v w) -> eq v w -> Not (gt v w) -> Trichotomous lt eq gt v w

MkGT : Not (lt v w) -> Not (eq v w) -> gt v w -> Trichotomous lt eq gt v w