Data.Prim.Bits64

Reexports

import public Algebra.Ring
import public Control.Order
import public Control.Relation
import public Control.Relation.ReflexiveClosure
import public Control.Relation.Trichotomy
import public Control.WellFounded
import public Data.Maybe0

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
Transitive Bits64 (<)
Trichotomous Bits64 (<)

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 (>) : Bits64 -> Bits64 -> Type

  Flipped version of `(<)`.

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

0 (<=) : Bits64 -> Bits64 -> Type

  Alias for `ReflexiveClosure (<) m n`

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

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

Totality: total
Visibility: public export

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

Totality: total
Visibility: public export

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) -> MinBits64 <= m

  `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

0 ltImpliesNatLT : (x : Bits64) -> (y : Bits64) -> x < y => lt (cast x) (cast y) = True

Totality: total
Visibility: export

0 lteImpliesNatLT : (x : Bits64) -> (y : Bits64) -> x <= y => lt (cast x) (S (cast y)) = True

Totality: total
Visibility: export

0 gtImpliesNatGT : (x : Bits64) -> (y : Bits64) -> x > y => gt (cast x) (cast y) = True

Totality: total
Visibility: export

bits64ToFin : (x : Bits64) -> (0 y : Bits64) -> {auto 0 _ : x < y} -> Fin (cast y)

Totality: total
Visibility: export

bits64ToFinLTE : (x : Bits64) -> (0 y : Bits64) -> {auto 0 _ : x <= y} -> Fin (S (cast y))

Totality: total
Visibility: export