Data.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)

toOrdering : Trichotomy lt m n -> Ordering

Totality: total
Visibility: public export