Exact hexadecimal external character sequences

IEEE 754 §5.12.3 uses a hexadecimal significand and a mandatory decimal binary exponent: -0x1.ap+3 denotes -13. The positional scanner, signs and exponent integer parser are shared with decimal input. No host floating point is used.

def FloatLib.Numerics.HexText.digitValue? (character : Char) : Option ℕ

Decode an ASCII hexadecimal digit, accepting either letter case.

def FloatLib.Numerics.HexText.parseExponent : List Char → Option ℤ

A hexadecimal exponent must have a p marker and a signed decimal integer.

def FloatLib.Numerics.HexText.parseCharacters (characters : List Char) : Option Dyadic

Decode a hexadecimal significand with a 0x prefix and p exponent to an exact signed dyadic.

def FloatLib.Numerics.HexText.parse (text : String) : Option Dyadic

Parse a hexadecimal external character sequence without discarding signed zero.

def FloatLib.Numerics.HexText.characters (value : Dyadic) : List Char

Exact IEEE hexadecimal spelling; the significand is integral and the exponent is binary.

def FloatLib.Numerics.HexText.format (value : Dyadic) : String

Exact hexadecimal output preserves all three dyadic fields.

def FloatLib.Numerics.HexText.radixPair (value : Dyadic) : ℕ × ℤ

Express the dyadic magnitude as a coefficient times an integral power of sixteen.

def FloatLib.Numerics.HexText.significant (roundMagnitude : Bool → ℚ → ℕ) (value : Dyadic) (digits : ℕ+) : Dyadic

Round to a requested hexadecimal digit count using the common radix precision algorithm.