Exact binary floating arithmetic for the reference lane. A format owns its
exponent/fraction widths, bias and rational scale. The operations round once
through the maintained literal-rounding specification, preserving subnormals
and signed zero. NaN selection is the reference policy (quiet first operand,
negative quiet NaN for invalid operations); it is not a hardware attestation.
This module is never part of a production device execution path.
The admitted reference formats are binary32Format and binary64Format;
new widths need their own rational-exponent bound and known-answer rows.
13family BinaryFloatFormat : Type 0
14constructor BinaryFloatFormatOf
15field unrestricted binaryFloatExponentWidth : Nat
16field unrestricted binaryFloatFractionWidth : Nat
17field unrestricted binaryFloatExponentBias : NatThe compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.