Control.Relation.TotalOrder

Irreflexive and trichomotomous relations, and total orders

Definitions

interface Irreflexive : (a : Type) -> (a -> a -> Type) -> Type

Parameters: a, r
Methods:

irrefl : r x x -> Void

Implementation: 

Irreflexive Nat LT

irrefl : Irreflexive a r => r x x -> Void

Visibility: public export

irrefl' : Irreflexive a r => r x y -> x = y -> Void

  Alternative version of irreflexivity

Visibility: public export

natIrrefl : LT x x -> Void

Visibility: public export

data Trichotomy : (0 _ : (a -> a -> Type)) -> a -> a -> Type

Totality: total
Visibility: public export
Constructors:

LT : r x y -> Trichotomy r x y

EQ : x = y -> Trichotomy r x y

GT : r y x -> Trichotomy r x y

interface Trichotomous : (a : Type) -> (a -> a -> Type) -> Type

Parameters: a, r
Methods:

trichotomy : (x : a) -> (y : a) -> Trichotomy r x y

Implementation: 

Trichotomous Nat LT

trichotomy : Trichotomous a r => (x : a) -> (y : a) -> Trichotomy r x y

Visibility: public export

trichotomySucc : Trichotomy LT m n -> Trichotomy LT (S m) (S n)

Visibility: public export

succLTE : LTE x y -> LTE x (S y)

Visibility: public export

precLTE : LTE (S x) y -> LTE x y

Visibility: public export

interface TotalOrder : (a : Type) -> (a -> a -> Type) -> Type

  Very similar to LinearOrder (in Control.TotalOrder) but based off LT rather than LTE

Parameters: a, r
Constraints: Irreflexive a r, Transitive a r, Trichotomous a r
Implementation: 

TotalOrder Nat LT