Idris2Doc : Decidable.Order

Decidable.Order

Congruence : (t : Type) -> (t -> t) -> (t -> t -> Type) -> Type
Parameters: t, f, eq
Constraints: Equivalence t eq
Methods:
congruent : (a : t) -> (b : t) -> eqab -> eq (fa) (fb)
total

Implementation: 
CongruencetfEqual
Equivalence : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, eq
Constraints: Preorder t eq
Methods:
symmetric : (a : t) -> (b : t) -> eqab -> eqba
total

Implementation: 
EquivalencetEqual
Ordered : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, to
Constraints: Poset t to
Methods:
order : (a : t) -> (b : t) -> Either (toab) (toba)
total

Implementations:
OrderedNatLTE
Ordered (Fink) FinLTE
Poset : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, po
Constraints: Preorder t po
Methods:
antisymmetric : (a : t) -> (b : t) -> poab -> poba -> _
total

Implementations:
PosetNatLTE
Poset (Fink) FinLTE
Preorder : (t : Type) -> (t -> t -> Type) -> Type
Parameters: t, po
Methods:
transitive : (a : t) -> (b : t) -> (c : t) -> poab -> pobc -> poac
total
reflexive : (a : t) -> poaa
total

Implementations:
PreorderNatLTE
PreordertEqual
Preorder (Fink) FinLTE
antisymmetric : Posettpo => (a : t) -> (b : t) -> poab -> poba -> a = b
congruent : Congruencetfeq => (a : t) -> (b : t) -> eqab -> eq (fa) (fb)
maximum : Orderedtto => t -> t -> t
minimum : Orderedtto => t -> t -> t
order : Orderedtto => (a : t) -> (b : t) -> Either (toab) (toba)
reflexive : Preordertpo => (a : t) -> poaa
symmetric : Equivalenceteq => (a : t) -> (b : t) -> eqab -> eqba
transitive : Preordertpo => (a : t) -> (b : t) -> (c : t) -> poab -> pobc -> poac