Idris2Doc : Data.Prim.Bits16

Data.Prim.Bits16

(source)
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 (<) : Bits16 -> Bits16 -> 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 Bits16 (<)
  
Trichotomous Bits16 (<)

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

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
0 (<=) : Bits16 -> Bits16 -> Type
  Alias for `ReflexiveClosure (<) m n`

  Totality: total
  Visibility: public export
  Fixity Declaration: infix operator, level 6
lt : (x : Bits16) -> (y : Bits16) -> Maybe0 (x < y)
  Totality: total
  Visibility: public export
lte : (x : Bits16) -> (y : Bits16) -> Maybe0 (x <= y)
  Totality: total
  Visibility: public export
comp : (m : Bits16) -> (n : Bits16) -> Trichotomy (<) m n
  Totality: total
  Visibility: export
MinBits16 : Bits16
  Lower bound of `Bits16`

  Totality: total
  Visibility: public export
MaxBits16 : Bits16
  Upper bound of `Bits16`

  Totality: total
  Visibility: public export
0 GTE_MinBits16 : (m : Bits16) -> MinBits16 <= m
  `m >= 0` for all `m` of type `Bits16`.

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

  Totality: total
  Visibility: export
0 LTE_MaxBits16 : (m : Bits16) -> m <= MaxBits16
  `m <= MaxBits16` for all `m` of type `Bits16`.

  Totality: total
  Visibility: export
0 Not_GT_MaxBits16 : m > MaxBits16 -> Void
  Not value of type `Bits16` is greater than `MaxBits16`.

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

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

  Totality: total
  Visibility: export
0 ltImpliesNatLT : (x : Bits16) -> (y : Bits16) -> x < y => lt (cast x) (cast y) = True
  Totality: total
  Visibility: export
0 lteImpliesNatLT : (x : Bits16) -> (y : Bits16) -> x <= y => lt (cast x) (S (cast y)) = True
  Totality: total
  Visibility: export
0 gtImpliesNatGT : (x : Bits16) -> (y : Bits16) -> x > y => gt (cast x) (cast y) = True
  Totality: total
  Visibility: export
bits16ToFin : (x : Bits16) -> (0 y : Bits16) -> {auto 0 _ : x < y} -> Fin (cast y)
  Totality: total
  Visibility: export
bits16ToFinLTE : (x : Bits16) -> (0 y : Bits16) -> {auto 0 _ : x <= y} -> Fin (S (cast y))
  Totality: total
  Visibility: export