Idris2Doc : Data.Order

Data.Order

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
Constructors:
MkLT : ltvw -> Not (eqvw) -> Not (gtvw) -> Trichotomouslteqgtvw
MkEQ : Not (ltvw) -> eqvw -> Not (gtvw) -> Trichotomouslteqgtvw
MkGT : Not (ltvw) -> Not (eqvw) -> gtvw -> Trichotomouslteqgtvw