Data.Prim.Integer

Reexports

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

Transitive Integer (<)

Trichotomous Integer (<)

Fixity Declaration: infix operator, level 6

unerase : (0 _ : m < n) -> m < n

  Makes a compile-time proof of `x < y` available at runtime.
  
  Heads up: `(<)` is not supposed to be used or even needed at runtime,
  as it will be erased anymay. However, this function is sometimes
  required, for instance when implementing interface `Connex`.

Totality: total
Visibility: export

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

  Alias for `ReflexiveClosure (<) m n`

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6

lt : (x : Integer) -> (y : Integer) -> Maybe0 (x < y)

Totality: total
Visibility: public export

lte : (x : Integer) -> (y : Integer) -> Maybe0 (x <= y)

Totality: total
Visibility: public export

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