Documentation

Natural numbers with an infinity element

Some algebraic properties of interest:

1 * x = x
x * (y * z) = (x * y) * z
0 * x = 0
x * y = y * x
x * (a + b) = x * a + x * b

Some algebraic properties of interest:

x ^ 0        = 1
x ^ (n + 1)  = x * (x ^ n)
x ^ (m + n)  = (x ^ m) * (x ^ n)
x ^ (m * n)  = (x ^ m) ^ n

nSub x y = Just z iff z is the unique value such that Add y z = Just x.

Rounds down.

y * q + r = x
x / y     = q with remainder r
0 <= r && r < y

We don't allow Inf in the first argument for two reasons: 1. It matches the behavior of nMod, 2. The well-formedness constraints can be expressed as a conjunction.

nCeilDiv msgLen blockSize computes the least n such that msgLen <= blockSize * n. It is undefined when blockSize = 0, or when blockSize = inf. inf divided by any positive finite value is inf.

nCeilMod msgLen blockSize computes the least k such that blockSize divides msgLen + k. It is undefined when blockSize = 0 or blockSize = inf. inf modulus any positive finite value is 0.

Rounds up. lg2 x = y, iff y is the smallest number such that x <= 2 ^ y

nWidth n is number of bits needed to represent all numbers from 0 to n, inclusive. nWidth x = nLg2 (x + 1).

length [ x, y .. z ]

Compute the logarithm of a number in the given base, rounded down to the closest integer. The boolean indicates if we the result is exact (i.e., True means no rounding happened, False means we rounded down). The logarithm base is the second argument.

Compute the number of bits required to represent the given integer.

Compute the exact root of a natural number. The second argument specifies which root we are computing.

Compute the the n-th root of a natural number, rounded down to the closest natural number. The boolean indicates if the result is exact (i.e., True means no rounding was done, False means rounded down). The second argument specifies which root we are computing.