Idris2Doc : Data.Prim.Bits16

Data.Prim.Bits16

(source)

Reexports

importpublic Control.WellFounded
importpublic Data.DPair
importpublic Data.Prim.Ord
importpublic Algebra.Solver.Ring

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
TotalBits16(<)
WellFoundedBits16(<)

Fixity Declaration: infix operator, level 6
0mkLT : (0_ : m<n=True) ->m<n
  Contructor for `(<)`.

This can only be used in an erased context.

Totality: total
Visibility: export
0runLT : 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
  `m <= n` mean that either `m < n` or `m === n` holds.

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

Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6
0(/=) : Bits16->Bits16->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 : Bits16) -> (n : Bits16) ->Trichotomy(<)mn
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
0GTE_MinBits16 : (m : Bits16) ->m>=MinBits16
  `m >= 0` for all `m` of type `Bits16`.

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

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

Totality: total
Visibility: export
0Not_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
sdiv : Bits16-> (d : Bits16) -> {auto0_ : 0<d} ->Bits16
  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 : Bits16) -> (d : Bits16) -> {auto0_ : 1<d} -> {auto0_ : 0<n} ->SubsetBits16 (\{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 : Bits16-> (d : Bits16) -> {auto0_ : 0<d} ->Bits16
  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 : Bits16-> (d : Bits16) -> {auto0_ : 0<d} ->SubsetBits16 (\{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