Idris2Doc : Data.Prim.Int32

Data.Prim.Int32

(source)
Reexports
import public Control.WellFounded
import public Data.DPair
import public Data.Prim.Ord
import public Algebra.Solver.Ring
Definitions
data (<) : Int32 -> Int32 -> 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 Int32 (<)
  
WellFounded Int32 (<)

  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 (>) : Int32 -> Int32 -> Type
  Flipped version of `(<)`.

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

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

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (/=) : Int32 -> Int32 -> 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 : Int32) -> (n : Int32) -> Trichotomy (<) m n
  Totality: total
  Visibility: export
MinInt32 : Int32
  Lower bound of `Int32`

  Totality: total
  Visibility: public export
MaxInt32 : Int32
  Upper bound of `Int32`

  Totality: total
  Visibility: public export
0 GTE_MinInt32 : (m : Int32) -> m >= MinInt32
  `m >= MinInt32` for all `m` of type `Int32`.

  Totality: total
  Visibility: export
0 Not_LT_MinInt32 : m < MinInt32 -> Void
  Not value of type `Int32` is less than zero.

  Totality: total
  Visibility: export
0 LTE_MaxInt32 : (m : Int32) -> m <= MaxInt32
  `m <= MaxInt32` for all `m` of type `Int32`.

  Totality: total
  Visibility: export
0 Not_GT_MaxInt32 : m > MaxInt32 -> Void
  Not value of type `Int32` is greater than `MaxInt32`.

  Totality: total
  Visibility: export
accessLT : (m : Int32) -> Accessible (<) m
  Every value of type `Int32` is accessible with relation
  to `(<)`.

  Totality: total
  Visibility: export
accessGT : (m : Int32) -> Accessible (>) m
  Every value of type `Int32` is accessible with relation
  to `(>)`.

  Totality: total
  Visibility: export
sdiv : Int32 -> (d : Int32) -> {auto 0 _ : d /= 0} -> Int32
  Safe division.

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

  Totality: total
  Visibility: export