Idris2Doc : Data.Int.Order

Data.Int.Order

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