digits, indexed by their base at the type level

digit x: construct a digit. 0 <= x < base must hold true.

Nicer if TypeApplications is enabled, then you can say:

>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> digit @9 8
Just 8 (base 9)

Like digit, but throws an ErrorCall if the value is out of range.

sample usage:

>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> digit' @9 7
7 (base 9)

getBase d: return the base of the digit d

getBaseT p: if p is of some type a base, then reflect the base into a value.

Useful for getting the base, just given a Proxy; e.g.:

>>> :set -XDataKinds
>>> :set -XTypeApplications
>>> let p = Proxy :: Proxy 3
>>> getBaseT p
3

Making Digit an instance of Num does not seem sensible, but it's nevertheless useful to be able to add and subtract digits, so <+> and <-> are provided for this.

a + b: Add a and b. Throws an ErrorCall if the result is out of range.

a - b: Subtract b from a. Throws an ErrorCall if the result is out of range.

This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.

Since: base-4.7.0.0