Idris2Doc : Data.Prim.Integer

Data.Prim.Integer

(source)
Reexports
import public Control.WellFounded
import public Data.Prim.Ord
import public Algebra.Solver.Ring
Definitions
data (<) : Integer -> Integer -> Type
  Witness that `m < n === True`.

  Totality: total
  Visibility: export
  Constructor: 
LT : (0 _ : m < n = True) -> m < n

  Hints:
  
(0 _ : m < n = True) -> m < n
  
Total Integer (<)

  Fixity Declaration: infix operator, level 6
0 mkLT : (0 _ : m < n = True) -> m < n
  Contructor for `(<)`.
  
  This can only be used in an erased context.

  Totality: total
  Visibility: export
0 runLT : m < n -> m < n = True
  Extractor for `(<)`.
  
  This can only be used in an erased context.

  Totality: total
  Visibility: export
strictLT : (0 _ : m < n) -> Lazy c -> c
  We don't trust values of type `(<)` too much,
  so we use this when creating magical results.

  Totality: total
  Visibility: export
0 (>) : Integer -> Integer -> Type
  Flipped version of `(<)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (<=) : Integer -> Integer -> Type
  `m <= n` mean that either `m < n` or `m === n` holds.

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (>=) : Integer -> Integer -> Type
  Flipped version of `(<=)`.

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (/=) : Integer -> Integer -> Type
  `m /= n` mean that either `m < n` or `m > n` holds.

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
comp : (m : Integer) -> (n : Integer) -> Trichotomy (<) m n
  Totality: total
  Visibility: export
0 plusGT : (k : Integer) -> (m : Integer) -> (n : Integer) -> k < m -> (n + k) < (n + m)
  This axiom, which only holds for unbounded integers, relates
  addition and the ordering of integers:
  
  From `k < m` follows `n + k < n + m` for all integers `k`, `m`, and `n`.

  Totality: total
  Visibility: export
0 multPosPosGT0 : (m : Integer) -> (n : Integer) -> 0 < m -> 0 < n -> 0 < (m * n)
  This axiom, which only holds for unbounded integers, relates
  multiplication and the ordering of integers:
  
  From `0 < m` and `0 < n` follows `0 < m * n` for all integers `m` and `n`.

  Totality: total
  Visibility: export
0 oneAfterZero : (n : Integer) -> 0 < n -> 1 <= n
  There is no integer between 0 and 1.

  Totality: total
  Visibility: export
0 modLT : (n : Integer) -> (d : Integer) -> 0 < d -> (0 <= (n `mod` d), (n `mod` d) < d)
  For positive `d`, `mod n d` is a non-negative number
  strictly smaller than `d`.

  Totality: total
  Visibility: export
0 modNegEQ : (n : Integer) -> (d : Integer) -> d < 0 -> n `mod` d = n `mod` neg d
  Totality: total
  Visibility: export
0 lawDivMod : (n : Integer) -> (d : Integer) -> d /= 0 -> (d * (n `div` d)) + (n `mod` d) = n
  Totality: total
  Visibility: export
sdiv : Integer -> (d : Integer) -> {auto 0 _ : d /= 0} -> Integer
  Safe division.

  Totality: total
  Visibility: export
smod : Integer -> (d : Integer) -> {auto 0 _ : d /= 0} -> Integer
  Safe modulo.

  Totality: total
  Visibility: export
0 BoundedLT : Integer -> Integer -> Integer -> Type
  Totality: total
  Visibility: public export
0 BoundedGT : Integer -> Integer -> Integer -> Type
  Totality: total
  Visibility: public export
accessLT : (m : Integer) -> Accessible (BoundedLT lb) m
  Every value of type `Integer` with a fixed lower bound
  is accessible with relation to `(<)`.

  Totality: total
  Visibility: export
accessGT : (m : Integer) -> Accessible (BoundedGT ub) m
  Every value of type `Integer` with a fixed upper bound
  is accessible with relation to `(>)`.

  Totality: total
  Visibility: export