Shared ASCII infinity and NaN spellings

The caller supplies the special-value constructors and interprets the diagnostic suffix. The scanner accepts case-independent Inf/Infinity/NaN/sNaN and decimal payload digits. An absent suffix denotes zero; the binding chooses its meaning.

def FloatLib.Numerics.SpecialText.consumeKeyword : List Char → List Char → Option (List Char)

Match a lowercase ASCII keyword case-insensitively, leaving the remaining characters unchanged.

def FloatLib.Numerics.SpecialText.parsePayload (characters : List Char) : Option ℕ

A missing diagnostic suffix denotes payload zero; otherwise every character must be a digit.

def FloatLib.Numerics.SpecialText.parseSpecial {α : Type} (infinity : Bool → α) (nan : Bool → Bool → ℕ → α) (negative : Bool) (characters : List Char) : Option α

Parse the unsigned part of a special value, consuming the entire input. The nan constructor receives the sign, signaling bit, and payload, in that order.

def FloatLib.Numerics.SpecialText.nanCharacters (negative signaling : Bool) (payload : ℕ) : List Char

Exact special output, retaining sign, signaling state, and diagnostic digits.

def FloatLib.Numerics.SpecialText.infinityCharacters (negative : Bool) : List Char

Infinity output preserves the sign and uses the full IEEE name.