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.
```

## Definitions

`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
Visibility: export
`data LT : Int -> Int -> Type`
`  `LT a b` is a proof that `a` is less than `b` which is to say that  the function call `a < b` returns `True`.    NB: we do not re-export the constructor so that users cannot force  our magic functions to blow up in absurd contexts by bypassing the  safety measures introduced by the `strictX` functions.  We do provide functions corresponding to the wrapping and unwrapping  of `LT` but, crucially, they do not let people force `LT` proofs to  be in canonical form.`

Totality: total
Visibility: export
Constructor:
`MkLT : a < b = True -> LT a b`
`mkLT : a < b = True -> LT a b`
`  We may prove `LT a b` by using a proof that `a < b` returns `True`.`

Totality: total
Visibility: export
`runLT : LT a b -> a < b = True`
`  From a proof that `LT a b`, we may concluded that `a < b` returns `True`.`

Totality: total
Visibility: export
`strictLT : LT a b -> Lazy c -> c`
`  Do not trust arbitrary `LT` proofs when manufacturing magic ones:  be strict!`

Totality: total
Visibility: export
`decide : (a : Int) -> (b : Int) -> Dec (LT a b)`
`  LT is decidable, by virtue of being the reflection of a boolean function`

Totality: total
Visibility: export
`trans : LT a b -> LT b c -> LT a (the Int c)`
`  LT is a transitive relation. This cannot be proven so we use a magic trick.`

Totality: total
Visibility: export
`irrefl : Not (LT a a)`
`  LT is an irreflexive relation.  The crash will never happen because the `LT a a` argument will never reduce  to a canonical form (unless the built-in function (<) is buggy).`

Totality: total
Visibility: export
`GT : Int -> Int -> Type`
`  GT is defined in terms of LT to avoid code duplication`

Totality: total
Visibility: public export
`LT_not_GT : LT a b -> Not (GT a b)`
Totality: total
Visibility: export
`GT_not_LT : GT a b -> Not (LT a b)`
Totality: total
Visibility: export
`data EQ : Int -> Int -> Type`
`  `EQ a b` is a proof that `a` is equal to `b` which is to say that  the function call `a == b` returns `True`.    NB: we do not re-export the constructor so that users cannot force  our magic functions to blow up in absurd contexts by bypassing the  safety measures introduced by the `strictX` functions.  We do provide functions corresponding to the wrapping and unwrapping  of `EQ` but, crucially, they do not let people force `EQ` proofs to  be in canonical form.`

Totality: total
Visibility: export
Constructor:
`MkEQ : a == b = True -> EQ a b`
`mkEQ : a == b = True -> EQ a b`
`  We may prove `EQ a b` by using a proof that `a == b` returns `True`.`

Totality: total
Visibility: export
`runEQ : EQ a b -> a == b = True`
`  From a proof that `EQ a b`, we may concluded that `a == b` returns `True`.`

Totality: total
Visibility: export
`strictEQ : EQ a b -> Lazy c -> c`
`  Do not trust arbitrary `EQ` proofs when manufacturing magic ones:  be strict!`

Totality: total
Visibility: export
`decide : (a : Int) -> (b : Int) -> Dec (EQ a b)`
`  EQ is decidable, by virtue of being the reflection of a boolean function`

Totality: total
Visibility: export
`refl : EQ a a`
`  EQ is a reflexive relation`

Totality: total
Visibility: export
`elimEQ : (0 p : (Int -> Type)) -> EQ a b -> p a -> p b`
`  EQ is substitutive`

Totality: total
Visibility: export
`reflect : EQ a b -> a = b`
`  EQ implies propositional equality`

Totality: total
Visibility: export
`sym : EQ a b -> EQ b a`
`  EQ is a symmetric relation`

Totality: total
Visibility: export
`trans : EQ a b -> EQ b c -> EQ a c`
`  EQ is a transitive relation`

Totality: total
Visibility: export
`trans_LT_EQ : LT a b -> EQ b c -> LT a c`
Totality: total
Visibility: export
`trans_EQ_LT : EQ a b -> LT b c -> LT a c`
Totality: total
Visibility: export
`LT_not_EQ : LT a b -> Not (EQ a b)`
Totality: total
Visibility: export
`EQ_not_LT : EQ a b -> Not (LT a b)`
Totality: total
Visibility: export
`EQ_not_GT : EQ a b -> Not (GT a b)`
Totality: total
Visibility: export
`GT_not_EQ : GT a b -> Not (EQ a b)`
Totality: total
Visibility: export
`data LTE : Int -> Int -> Type`
`  `LTE a b` is a proof that `a` is less or equal to `b` which is to say that  the function call `a < b` or `a == b` returns `True`.    NB: we do not re-export the constructor so that users cannot force  our magic functions to blow up in absurd contexts by bypassing the  safety measures introduced by the `strictX` functions.`

Totality: total
Visibility: export
Constructors:
`MkLT : a < b = True -> LTE a b`
`MkEQ : a == b = True -> LTE a b`
`runLTE : LTE a b -> Either (LT a b) (EQ a b)`
`  Unwrap an LTE proof to get either an LT or an EQ one`

Totality: total
Visibility: export
`strictLTE : LTE a b -> Lazy c -> c`
`  Do not trust arbitrary `LTE` proofs when manufacturing magic ones:  be strict!`

Totality: total
Visibility: export
`decide : (a : Int) -> (b : Int) -> Dec (LTE a b)`
`  LTE is decidable by virture of both LT and EQ being decidable`

Totality: total
Visibility: export
`refl : LTE a a`
`  LTE is a reflexive relation`

Totality: total
Visibility: export
`trans_LT_LTE : LT a b -> LTE b c -> LT a c`
Totality: total
Visibility: export
`trans_LTE_LT : LTE a b -> LT b c -> LT a c`
Totality: total
Visibility: export
`inject_LT_LTE : LT a b -> LTE a b`
Totality: total
Visibility: export
`inject_EQ_LTE : EQ a b -> LTE a b`
Totality: total
Visibility: export
`trans : LTE a b -> LTE b c -> LTE a c`
`  LTE is a transitive relation`

Totality: total
Visibility: export
`antisym : LTE a b -> LTE b a -> EQ a b`
`  LTE is an antisymmetric relation`

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

Totality: total
Visibility: public export
`trichotomous : (a : Int) -> (b : Int) -> Trichotomous LT EQ GT a b`
`  Any pair of Ints is related either via LT, EQ, or GT`

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

Totality: total
Visibility: export
`decide_LTE_GT : (a : Int) -> (b : Int) -> Either (LTE a b) (GT a b)`
`  Any pair of Ints is related either via LTE or GT`

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

Totality: total
Visibility: export
`pred_LT_LTE : LT a b -> LTE a (b - 1)`
`  Subtracting one to a strictly larger Int, yields a larger Int`

Totality: total
Visibility: export
`sucBounded : LT a b -> LT a (a + 1)`
`  Adding one to an Int yields a strictly larger one,  provided there is no overflow`

Totality: total
Visibility: export