Idris2Doc : Control.Order

Control.Order

An order is a particular kind of binary relation. The order
relation is intended to proceed in some direction, though not
necessarily with a unique path.

Orders are often defined simply as bundles of binary relation
properties.

A prominent example of an order relation is LTE over Nat.

Definitions

interfacePreorder : (ty : Type) -> (ty->ty->Type) ->Type
  A preorder is reflexive and transitive.

Parameters: ty, rel
Constraints: Reflexive ty rel, Transitive ty rel
Implementation: 
PreorderNatLTE
interfacePartialOrder : (ty : Type) -> (ty->ty->Type) ->Type
  A partial order is an antisymmetrics preorder.

Parameters: ty, rel
Constraints: Preorder ty rel, Antisymmetric ty rel
Implementation: 
PartialOrderNatLTE
interfaceConnex : (ty : Type) -> (ty->ty->Type) ->Type
  A relation is connex if for any two distinct x and y, either x ~ y or y ~ x.

This can also be stated as a trichotomy: x ~ y or x = y or y ~ x.

Parameters: ty, rel
Methods:
connex : Not (x=y) ->Either (relxy) (relyx)

Implementation: 
ConnexNatLTE
connex : Connextyrel=>Not (x=y) ->Either (relxy) (relyx)
Visibility: public export
interfaceStronglyConnex : (ty : Type) -> (ty->ty->Type) ->Type
  A relation is strongly connex if for any two x and y, either x ~ y or y ~ x.

Parameters: ty, rel
Methods:
order : (x : ty) -> (y : ty) ->Either (relxy) (relyx)
order : StronglyConnextyrel=> (x : ty) -> (y : ty) ->Either (relxy) (relyx)
Visibility: public export
interfaceLinearOrder : (ty : Type) -> (ty->ty->Type) ->Type
  A linear order is a connex partial order.

Parameters: ty, rel
Constraints: PartialOrder ty rel, Connex ty rel
Implementation: 
LinearOrderNatLTE