Idris2Doc : Decidable.Order.Strict

Decidable.Order.Strict

DecOrdering : t -> t -> Type
Totality: total
Constructors:
DecLT : ltab -> DecOrderingab
DecEQ : a = b -> DecOrderingab
DecGT : ltba -> DecOrderingab
EqOr : (spo : (t -> t -> Type)) -> StrictPreordertspo => t -> t -> Type
Totality: total
InferOrder : {auto {conArg:1117} : StrictOrderedtspo} -> OrderedtEqOrspo
Totality: total
InferPoset : {auto {conArg:870} : StrictPreordertspo} -> PosettEqOrspo
Totality: total
No documentation for Decidable.Order.Strict.MkPreorder
StrictOrdered : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, spo
Constraints: StrictPreorder t spo
Methods:
order : (a : t) -> (b : t) -> DecOrderingab

Implementation: 
StrictOrderedNatLT
StrictPreorder : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, spo
Methods:
transitive : (a : t) -> (b : t) -> (c : t) -> spoab -> spobc -> spoac
irreflexive : (a : t) -> Not (spoaa)

Implementation: 
StrictPreorderNatLT
asymmetric : StrictPreordertspo => (a : t) -> (b : t) -> spoab -> Not (spoba)
Totality: total
irreflexive : StrictPreordertspo => (a : t) -> Not (spoaa)
Totality: total
order : StrictOrderedtspo => (a : t) -> (b : t) -> DecOrderingab
Totality: total
transitive : StrictPreordertspo => (a : t) -> (b : t) -> (c : t) -> spoab -> spobc -> spoac
Totality: total