Idris2Doc : Data.Prim.Bits64

Data.Prim.Bits64

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

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

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

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

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

  Totality: total
  Visibility: public export
MaxBits64 : Bits64
  Upper bound of `Bits64`

  Totality: total
  Visibility: public export
0 GTE_MinBits64 : (m : Bits64) -> m >= MinBits64
  `m >= 0` for all `m` of type `Bits64`.

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

  Totality: total
  Visibility: export
0 LTE_MaxBits64 : (m : Bits64) -> m <= MaxBits64
  `m <= MaxBits64` for all `m` of type `Bits64`.

  Totality: total
  Visibility: export
0 Not_GT_MaxBits64 : m > MaxBits64 -> Void
  Not value of type `Bits64` is greater than `MaxBits64`.

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

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

  Totality: total
  Visibility: export
sdiv : Bits64 -> (d : Bits64) -> {auto 0 _ : 0 < d} -> Bits64
  Safe division.
  
  This uses `0 < d` as a constraint instead
  of `0 /= d`, because in my experience, the former
  is much more useful.

  Totality: total
  Visibility: export
rdiv : (n : Bits64) -> (d : Bits64) -> {auto 0 _ : 1 < d} -> {auto 0 _ : 0 < n} -> Subset Bits64 (\{arg:0} => {arg:0} < n)
  Refined division.
  
  This comes with a proof that the result is
  strictly smaller than `n`.
  
  This uses `0 < n` as a constraint instead
  of `0 /= n`, because in my experience, the former
  is much more useful.

  Totality: total
  Visibility: export
smod : Bits64 -> (d : Bits64) -> {auto 0 _ : 0 < d} -> Bits64
  Safe modulo.
  
  This uses `0 < d` as a constraint instead
  of `0 /= d`, because in my experience, the former
  is much more useful.
  
  If you need the postcondition that the result is strictly
  smaller than `d`, use `rmod` instead.

  Totality: total
  Visibility: export
rmod : Bits64 -> (d : Bits64) -> {auto 0 _ : 0 < d} -> Subset Bits64 (\{arg:0} => {arg:0} < d)
  Refined modulo.
  
  This comes with a proof that the result is strictly smaller
  than `d`.
  
  It uses `0 < d` as a constraint instead
  of `0 /= d`, because in my experience, the former
  is much more useful.

  Totality: total
  Visibility: export