Signed zero and its preferred quantum #
Every zero projects exactly with the supplied sign and the preferred exponent clamped to the representable exponent interval. No exception is raised, even when clamping changes its representation.
theorem
FloatLib.Floats.Formats.DecimalInterchange.projectMagnitude_zero
(f : Format)
(mode : RoundingMode)
(s : Bool)
(preferred : ℤ)
:
projectMagnitude f mode s 0 preferred = { value := Datum.finite s 0 (max f.minQuantum (min preferred f.maxQuantum)) }
An exact zero retains its sign and chooses the closest representable preferred exponent.
theorem
FloatLib.Floats.Formats.DecimalInterchange.project_zero
(f : Format)
(mode : RoundingMode)
(s : Bool)
(preferred : ℤ)
:
project f mode 0 preferred s = { value := Datum.finite s 0 (max f.minQuantum (min preferred f.maxQuantum)) }