Idris2Doc : Data.Prim.Ord

Data.Prim.Ord

(source)
Axioms and propsitions for primitive types with an
`Ord` implementation.

Reexports

import public Data.Trichotomy

Definitions

data Either0 : Type -> Type -> Type
  Similar to `Either` but with erased fields.

Totality: total
Visibility: public export
Constructors:
Left0 : (0 _ : a) -> Either0 a b
Right0 : (0 _ : b) -> Either0 a b
strictRefl : (0 _ : a = b) -> Lazy c -> c
  We often don't trust values of type `a === b`, as they might
  have been magically crafted using `believe_me` or `assert_total`
  followed by `idris_crash`. If a value of another type follows
  from a (potentially) magically crafted one, we only want the
  second value to reduce at compile time, if the first value
  reduces to `Refl`. Otherwise, we risk blowing up the compiler
  in an absurd context.

Totality: total
Visibility: export
interface Total : (a : Type) -> (a -> a -> Type) -> Type
  This interface is a witness that the given primitive type
  comes with a relation `lt`, with `lt` being a strict total order.
  We typically define the following aliases
  (or name the relation accordingly):
  
    `m < n`  := lt m n
    `m > n`  := lt n m
    `m <= n` := Either (lt m n) (m === n)
    `m >= n` := Either (lt n m) (n === m)
    `m /= n` := Either (lt m n) (lt n m)
  
  The following axioms must hold:
    1. (<) is transitive: From `k < m` and `m < n` follows `k < n`.
  
    2. Trichotomy: For all values `m` and `n` exactly one of the
       following holds: `m < n`, `m === n`, or `n < m`.
  
  It is in the nature of a primitive that we can't proof these axioms
  in Idris itself. We must therefore assume that they hold on all backends,
  and it is the responsibility of programmers implementing
  interface `Total` to make sure that the axioms actually hold.

Parameters: a, lt
Methods:
0 transLT : lt k m -> lt m n -> lt k n
  Axiom I: `<` is transitive.
trichotomy : (m : a) -> (n : a) -> Trichotomy lt m n
  Axiom II: Trichotomy of `<`, `===`, and `>`.

Implementations:
Total Integer (<)
Total Int (<)
Total Char (<)
Total Bits8 (<)
Total Bits16 (<)
Total Bits32 (<)
Total Bits64 (<)
Total Int8 (<)
Total Int16 (<)
Total Int32 (<)
Total Int64 (<)
Total String (<)
Total a lt => Total (Maybe a) (LT lt)
Total a lt => Total (Maybe a) (LT lt)
0 transLT : Total a lt => lt k m -> lt m n -> lt k n
  Axiom I: `<` is transitive.

Totality: total
Visibility: public export
trichotomy : Total a lt => (m : a) -> (n : a) -> Trichotomy lt m n
  Axiom II: Trichotomy of `<`, `===`, and `>`.

Totality: total
Visibility: public export
testLT : Total a lt => (x : a) -> (y : a) -> Either0 (lt x y) (Either (lt y x) (y = x))
  Tests if the first value is strictly less than the second or not

Totality: total
Visibility: export
testGT : Total a lt => (x : a) -> (y : a) -> Either0 (lt y x) (Either (lt x y) (x = y))
  Tests if the first value is strictly greater than the second or not

Totality: total
Visibility: export
testEQ : Total a lt => (x : a) -> (y : a) -> Either0 (x = y) (Either (lt x y) (lt y x))
  Tests if the two values are provably equal or not

Totality: total
Visibility: export
0 irrefl : Total a lt => Not (lt m m)
  `<` is irreflexive.

Totality: total
Visibility: export
0 trans : Total a lt => lt k m -> lt m n -> lt k n
  This is an alias for `transLT`

Totality: total
Visibility: export
0 trans_EQ_NEQ : Total a lt => k = m -> Either (lt m n) (lt n m) -> Either (lt k n) (lt n k)
  `k === m` and `m /= n` implies `k /= n`.

Totality: total
Visibility: export
0 trans_NEQ_EQ : Total a lt => Either (lt k m) (lt m k) -> m = n -> Either (lt k n) (lt n k)
  `k === m` and `m /= n` implies `k /= n`.

Totality: total
Visibility: export
0 trans_LT_EQ : Total a lt => lt k m -> m = n -> lt k n
  `k < m` and `m === n` implies `k < n`

Totality: total
Visibility: export
0 trans_EQ_LT : Total a lt => k = m -> lt m n -> lt k n
  `k === m` and `m < n` implies `k < n`

Totality: total
Visibility: export
0 trans_LTE_LT : Total a lt => Either (lt k m) (k = m) -> lt m n -> lt k n
  `k <= m` and `m < n` implies `k < n`

Totality: total
Visibility: export
0 trans_LT_LTE : Total a lt => lt k m -> Either (lt m n) (m = n) -> lt k n
  `k < m` and `m <= n` implies `k < n`

Totality: total
Visibility: export
0 trans_GT_EQ : Total a lt => lt m k -> m = n -> lt n k
  `k > m` and `m === n` implies `k > n`

Totality: total
Visibility: export
0 trans_EQ_GT : Total a lt => k = m -> lt n m -> lt n k
  `k === m` and `m > n` implies `k > n`

Totality: total
Visibility: export
0 trans_GTE_GT : Total a lt => Either (lt m k) (m = k) -> lt n m -> lt n k
  `k >= m` and `m > n` implies `k > n`

Totality: total
Visibility: export
0 trans_GT_GTE : Total a lt => lt m k -> Either (lt n m) (n = m) -> lt n k
  `k > m` and `m >= n` implies `k > n`

Totality: total
Visibility: export
0 refl : Total a lt => Either (lt m m) (m = m)
  `<=` is reflexive.

Totality: total
Visibility: export
0 trans : Total a lt => Either (lt k m) (k = m) -> Either (lt m n) (m = n) -> Either (lt k n) (k = n)
  `<=` is transitive.

Totality: total
Visibility: export
0 antisym : Total a lt => Either (lt m n) (m = n) -> Either (lt n m) (m = n) -> m = n
  `<=` is antisymmetric.

Totality: total
Visibility: export
0 trans_LTE_EQ : Total a lt => Either (lt k m) (k = m) -> m = n -> Either (lt k n) (k = n)
  `k <= m` and `m === n` implies `k <= n`

Totality: total
Visibility: export
0 trans_EQ_LTE : Total a lt => k = m -> Either (lt m n) (m = n) -> Either (lt k n) (k = n)
  `k === m` and `m <= n` implies `(k <= n)`

Totality: total
Visibility: export
0 trans : Total a lt => Either (lt m k) (m = k) -> Either (lt n m) (n = m) -> Either (lt n k) (n = k)
  `>=` is transitive.

Totality: total
Visibility: export
0 antisym : Total a lt => Either (lt n m) (m = n) -> Either (lt m n) (m = n) -> m = n
  `>=` is antisymmetric.

Totality: total
Visibility: export
0 trans_GTE_EQ : Total a lt => Either (lt m k) (m = k) -> m = n -> Either (lt n k) (n = k)
  `k >= m` and `m === n` implies `k >= n`

Totality: total
Visibility: export
0 trans_EQ_GTE : Total a lt => k = m -> Either (lt n m) (n = m) -> Either (lt n k) (n = k)
  `k === m` and `m <= n` implies `(k <= n)`

Totality: total
Visibility: export
0 LT_not_GT : Total a lt => lt m n -> Not (lt n m)
  `m < n` implies `Not (m > n)`.

Totality: total
Visibility: export
0 LT_not_EQ : Total a lt => lt m n -> Not (m = n)
  `m < n` implies `Not (m === n)`.

Totality: total
Visibility: export
0 LT_not_GTE : Total a lt => lt m n -> Not (Either (lt n m) (n = m))
  `m < n` implies `Not (m >= n)`.

Totality: total
Visibility: export
0 Not_LT_to_GTE : Total a lt => Not (lt m n) -> Either (lt n m) (n = m)
  `Not (m < n)` implies `m >= n`.

Totality: total
Visibility: export
0 EQ_not_LT : Total a lt => m = n -> Not (lt m n)
  `m === n` implies `Not (m < n)`.

Totality: total
Visibility: export
0 EQ_not_GT : Total a lt => m = n -> Not (lt n m)
  `m === n` implies `Not (m > n)`.

Totality: total
Visibility: export
0 EQ_not_NEQ : Total a lt => m = n -> Not (Either (lt m n) (lt n m))
  `m === n` implies `Not (m /= n)`.

Totality: total
Visibility: export
0 Not_EQ_to_NEQ : Total a lt => Not (m = n) -> Either (lt m n) (lt n m)
  `Not (m < n)` implies `m /= n`.

Totality: total
Visibility: export
0 GT_not_LT : Total a lt => lt n m -> Not (lt m n)
  `m > n` implies `Not (m < n)`.

Totality: total
Visibility: export
0 GT_not_EQ : Total a lt => lt n m -> Not (m = n)
  `m > n` implies `Not (m === n)`.

Totality: total
Visibility: export
0 GT_not_LTE : Total a lt => lt n m -> Not (Either (lt m n) (m = n))
  `m > n` implies `Not (m <= n)`.

Totality: total
Visibility: export
0 Not_GT_to_LTE : Total a lt => Not (lt n m) -> Either (lt m n) (m = n)
  `Not (m > n)` implies `m <= n`.

Totality: total
Visibility: export
0 LTE_not_GT : Total a lt => Either (lt m n) (m = n) -> Not (lt n m)
  `m <= n` implies `Not (m > n)`.

Totality: total
Visibility: export
0 Not_LTE_to_GT : Total a lt => Not (Either (lt m n) (m = n)) -> lt n m
  `Not (m <= n)` implies `m > n`.

Totality: total
Visibility: export
0 LTE_and_GTE_to_EQ : Total a lt => Either (lt m n) (m = n) -> Either (lt n m) (n = m) -> m = n
  `m <= n` and `m >= n` implies `m === n`.

Totality: total
Visibility: export
0 LTE_and_NEQ_to_LT : Total a lt => Either (lt m n) (m = n) -> Either (lt m n) (lt n m) -> lt m n
  `m <= n` and `m /= n` implies `m < n`.

Totality: total
Visibility: export
0 NEQ_not_EQ : Total a lt => Either (lt m n) (lt n m) -> Not (m = n)
  `m /= n` implies `Not (m === n)`.

Totality: total
Visibility: export
0 Not_NEQ_to_EQ : Total a lt => Not (Either (lt m n) (lt n m)) -> m = n
  `Not (m /= n)` implies `m === n`.

Totality: total
Visibility: export
0 NEQ_and_LTE_to_LT : Total a lt => Either (lt m n) (lt n m) -> Either (lt m n) (m = n) -> lt m n
  `m /= n` and `m <= n` implies `m < n`.

Totality: total
Visibility: export
0 NEQ_and_GTE_to_GT : Total a lt => Either (lt m n) (lt n m) -> Either (lt n m) (n = m) -> lt n m
  `m /= n` and `m <= n` implies `m < n`.

Totality: total
Visibility: export
0 GTE_not_LT : Total a lt => Either (lt n m) (n = m) -> Not (lt m n)
  `m >= n` implies `Not (m < n)`.

Totality: total
Visibility: export
0 Not_GTE_to_LT : Total a lt => Not (Either (lt n m) (n = m)) -> lt m n
  `Not (m >= n)` implies `m < n`.

Totality: total
Visibility: export
0 GTE_and_LTE_to_EQ : Total a lt => Either (lt n m) (n = m) -> Either (lt m n) (m = n) -> m = n
  `m >= n` and `m <= n` implies `m === n`.

Totality: total
Visibility: export
0 GTE_and_NEQ_to_GT : Total a lt => Either (lt n m) (n = m) -> Either (lt m n) (lt n m) -> lt n m
  `m >= n` and `m /= n` implies `m > n`.

Totality: total
Visibility: export