Idris2Doc : Data.Int.Order

Data.Int.Order

Implementation of ordering relations for the primitive type `Int`
This is full of tricks as `Int` is a primitive type that can only
be interacted with using either literals or built-in functions.
The exported interface should however be safe.
EQ_not_GT : EQab -> Not (GTab)
Totality: total
EQ_not_LT : EQab -> Not (LTab)
Totality: total
GT : Int -> Int -> Type
  GT is defined in terms of LT to avoid code duplication

Totality: total
GTE : Int -> Int -> Type
  GTE is defined in terms of LTE to avoid code duplication

Totality: total
GT_not_EQ : GTab -> Not (EQab)
Totality: total
GT_not_LT : GTab -> Not (LTab)
Totality: total
LT_not_EQ : LTab -> Not (EQab)
Totality: total
LT_not_GT : LTab -> Not (GTab)
Totality: total
decide_LTE_GT : (a : Int) -> (b : Int) -> Either (LTEab) (GTab)
  Any pair of Ints is related either via LTE or GT

Totality: total
decide_LT_GTE : (a : Int) -> (b : Int) -> Either (LTab) (GTEab)
  Any pair of Ints is related either via LT or GTE

Totality: total
pred_LT_LTE : LTab -> LTEa (b-1)
  Subtracting one to a strictly larger Int, yields a larger Int

Totality: total
strictRefl : a = b -> Lazy c -> c
  Pattern-match on an equality proof so that the second argument to
strictRefl is only returned once the first is canonical.

Totality: total
sucBounded : LTab -> LTa (a+1)
  Adding one to an Int yields a strictly larger one,
provided there is no overflow

Totality: total
suc_LT_LTE : LTab -> LTE (a+1) b
  Adding one to a strictly smaller Int, yields a smaller Int

Totality: total
trans_EQ_LT : EQab -> LTbc -> LTac
Totality: total
trans_LT_EQ : LTab -> EQbc -> LTac
Totality: total
trichotomous : (a : Int) -> (b : Int) -> TrichotomousLTEQGTab
  Any pair of Ints is related either via LT, EQ, or GT

Totality: total