Positional character conversion

Printing and scanning share an explicit radix. The scanner accepts a digit decoder and leaves the first nondigit and its suffix unconsumed. Magnitude parsing adds a radix point and delegates exponent syntax to its caller; fractional digits each subtract fractionScale exponent units. Decimal and hexadecimal text use the same implementation with different syntax parameters.

def FloatLib.Numerics.RadixText.naturalDigits (value radix : ℕ) : List Char

Digits in printing order, including one digit for zero.

def FloatLib.Numerics.RadixText.scanDigits (characters : List Char) (accumulator radix : ℕ) (readDigit : Char → Option ℕ) : ℕ × ℕ × List Char

Read a maximal digit prefix, returning its value, length, and unconsumed suffix.

def FloatLib.Numerics.RadixText.parseMagnitude (characters : List Char) (radix : ℕ) (readDigit : Char → Option ℕ) (readExponent : List Char → Option ℤ) (fractionScale : ℤ) : Option (ℕ × ℤ)

Parse an unsigned significand and exponent with caller-supplied radix and exponent syntax.