Idris2Doc : Decidable.Order.Strict

Decidable.Order.Strict

An strict preorder (sometimes known as a quasi-order, or an
ordering) is what you get when you remove the diagonal `{(a,b) | a
r b , b r a}` from a preorder. For example a < b is an ordering.
This module extends base's Control.Order with the strict versions.
The interface system seems to struggle a bit with some of the constructions,
so I hacked them a bit. Sorry.
interfaceAsymmetric : (ty : Type) -> (ty -> ty -> Type) -> Type
Parameters: ty, rel
Methods:
asymmetric : relxy -> Not (relyx)
dataDecOrdering : t -> t -> Type
Totality: total
Constructors:
DecLT : ltab -> DecOrderingab
DecEQ : a = b -> DecOrderingab
DecGT : ltba -> DecOrderingab
recordEqOr : Relt -> t -> t -> Type
Totality: total
Constructor: 
MkEqOr : Either (a = b) (spoab) -> EqOrspoab

Projection: 
.runEqOr : EqOrspoab -> Either (a = b) (spoab)
interfaceIrreflexive : (ty : Type) -> (ty -> ty -> Type) -> Type
Parameters: ty, rel
Methods:
irreflexive : Not (relxx)

Implementation: 
IrreflexiveNatLT
interfaceStrictOrdered : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, spo
Constraints: StrictPreorder t spo
Methods:
order : (a : t) -> (b : t) -> DecOrderingab

Implementation: 
StrictOrderedNatLT
interfaceStrictPreorder : (ty : Type) -> (ty -> ty -> Type) -> Type
Parameters: ty, rel
Constraints: Transitive ty rel, Irreflexive ty rel
Implementation: 
StrictPreorderNatLT
asymmetric : Asymmetrictyrel => relxy -> Not (relyx)
Totality: total
irreflexive : Irreflexivetyrel => Not (relxx)
Totality: total
order : StrictOrderedtspo => (a : t) -> (b : t) -> DecOrderingab
Totality: total