Control.Relation.Trichotomy

Definitions

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

  Trichotomy formalises the fact that three relations are mutually
  exclusive. A value of type `Trichotomy lt m n` proofs, that
  exactly one of the relations `lt m n`, `m === n`, or `lt n m` holds.
  
  All proofs held by a value of type `Trichotomous` are erased, so
  at runtime such values get optimized to numbers 0, 1, or 2
  respectively.

Totality: total
Visibility: public export
Constructors:

LT : (0 _ : lt v w) -> (0 _ : Not (v = w)) -> (0 _ : Not (lt w v)) -> Trichotomy lt v w

EQ : (0 _ : Not (lt v w)) -> (0 _ : v = w) -> (0 _ : Not (lt w v)) -> Trichotomy lt v w

GT : (0 _ : Not (lt v w)) -> (0 _ : Not (v = w)) -> (0 _ : lt w v) -> Trichotomy lt v w

Hints:

Eq (Trichotomy lt m n)

Ord (Trichotomy lt m n)

Show (Trichotomy lt m n)

conIndex : Trichotomy lt m n -> Bits8

Totality: total
Visibility: public export

toOrdering : Trichotomy lt m n -> Ordering

Totality: total
Visibility: public export

swap : Trichotomy lt m n -> Trichotomy lt n m

Totality: total
Visibility: public export

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

Parameters: a, rel
Constructor: 

MkTrichotomous

Methods:

trichotomy : (m : a) -> (n : a) -> Trichotomy rel m n

Implementation: 

Strict a rel -> Trichotomous a rel

trichotomy : Trichotomous a rel => (m : a) -> (n : a) -> Trichotomy rel m n

Totality: total
Visibility: public export

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

Parameters: a, rel
Constraints: Transitive a rel, Trichotomous a rel
Constructor: 

MkStrict

0 irreflexive : Trichotomous a rel => rel x x -> Void

Totality: total
Visibility: public export

0 Not_LT_and_GT : Trichotomous a lt => lt m n -> Not (lt n m)

  `m < n` implies `Not (m > n)`.

Totality: total
Visibility: export

0 Not_LT_and_EQ : Trichotomous a lt => lt m n -> Not (m = n)

  `m < n` implies `Not (m === n)`.

Totality: total
Visibility: export

0 Not_LT_and_GTE : Trichotomous a lt => lt m n -> Not (ReflexiveClosure lt n m)

  `m < n` implies `Not (m >= n)`.

Totality: total
Visibility: export