Adjacent decimal values

IEEE 754-2019 §5.3.1 requires the nearest strictly greater or smaller value, selecting the least quantum in its cohort. Normalizing the input to its finest grid makes this a coefficient step. At a power of ten, the downward step uses the finer grid. No rounding direction is consulted.

Crossing the finite range or reaching a subnormal raises no exception. Only signaling NaNs raise invalid; NaN propagation otherwise follows the arithmetic payload policy.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborAbove (f : Format) (c : ℕ) (q : ℤ) : Datum

Positive successor of a finite value already on its least quantum.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.neighborBelow (f : Format) (c : ℕ) (q : ℤ) : Datum

Positive predecessor, using the finer grid immediately below a radix power.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextUp (f : Format) : Datum → Outcome

Least representable value strictly greater than the operand, except at positive infinity.

def FloatLib.Floats.Formats.DecimalInterchange.Arithmetic.nextDown (f : Format) (x : Datum) : Outcome

Greatest representable value strictly smaller than the operand, except at negative infinity.