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
Total Bits16 (<)
WellFounded Bits16 (<)
Fixity Declaration: infix operator, level 60 mkLT : (0 _ : m < n = True) -> m < n
Contructor for `(<)`.
This can only be used in an erased context.
Totality: total
Visibility: export0 runLT : m < n -> m < n = True
Extractor for `(<)`.
This can only be used in an erased context.
Totality: total
Visibility: exportstrictLT : (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: export0 (>) : Bits16 -> Bits16 -> Type
Flipped version of `(<)`.
Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 60 (<=) : Bits16 -> Bits16 -> Type
`m <= n` mean that either `m < n` or `m === n` holds.
Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 60 (>=) : Bits16 -> Bits16 -> Type
Flipped version of `(<=)`.
Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 60 (/=) : Bits16 -> Bits16 -> Type
`m /= n` mean that either `m < n` or `m > n` holds.
Totality: total
Visibility: public export
Fixity Declaration: infix operator, level 6comp : (m : Bits16) -> (n : Bits16) -> Trichotomy (<) m n
- Totality: total
Visibility: export MinBits16 : Bits16
Lower bound of `Bits16`
Totality: total
Visibility: public exportMaxBits16 : Bits16
Upper bound of `Bits16`
Totality: total
Visibility: public export0 GTE_MinBits16 : (m : Bits16) -> m >= MinBits16
`m >= 0` for all `m` of type `Bits16`.
Totality: total
Visibility: export0 Not_LT_MinBits16 : m < 0 -> Void
Not value of type `Bits16` is less than zero.
Totality: total
Visibility: export0 LTE_MaxBits16 : (m : Bits16) -> m <= MaxBits16
`m <= MaxBits16` for all `m` of type `Bits16`.
Totality: total
Visibility: export0 Not_GT_MaxBits16 : m > MaxBits16 -> Void
Not value of type `Bits16` is greater than `MaxBits16`
Totality: total
Visibility: exportaccessLT : (m : Bits16) -> Accessible (<) m
Every value of type `Bits16` is accessible with relation
to `(<)`.
Totality: total
Visibility: exportaccessGT : (m : Bits16) -> Accessible (>) m
Every value of type `Bits16` is accessible with relation
to `(>)`.
Totality: total
Visibility: exportsdiv : Bits16 -> (d : Bits16) -> {auto 0 _ : 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: exportrdiv : (n : Bits16) -> (d : Bits16) -> {auto 0 _ : 1 < d} -> {auto 0 _ : 0 < n} -> Subset Bits16 (\{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: exportsmod : Bits16 -> (d : Bits16) -> {auto 0 _ : 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: exportrmod : Bits16 -> (d : Bits16) -> {auto 0 _ : 0 < d} -> Subset Bits16 (\{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