Selecting an exact result's cohort

IEEE 754-2019 §5.2 selects the member nearest the preferred exponent. Starting at the smallest representable exponent, remove only exact trailing zeros, up to the preferred exponent or the largest stored quantum. Zero has a direct path, so a large distance between exponents does not cause a long recursion.

def FloatLib.Floats.Formats.DecimalInterchange.stripTrailing : ℕ → ℕ → ℕ × ℕ

Remove at most fuel exact trailing coefficient zeros. The second component counts the removed zeros.

def FloatLib.Floats.Formats.DecimalInterchange.preferredCohort (f : Format) (negative : Bool) (c : ℕ) (q preferred : ℤ) : Datum

Raise an exact result's quantum toward its preferred exponent without changing its value. The input quantum is already the smallest representable one for this coefficient.