Ordinary Lean instances for configured binary values #
Configured binary values ExecFloat (Configured.Family format code plan) receive the ordinary
Lean interfaces here, generically in the storage codec, so byte, machine-word, and wide carriers
share one set of instances. Numerical literals are rounded once from exact rationals. Display,
comparison, equality, and hashing operate on the exact-width model, independently of the packed
carrier.
Two different notions of equality are installed and callers must keep them apart.
==(BEq) is IEEE numerical equality throughExecFloat.compareEqual:NaN == NaNisfalseand-0 == +0istruewhen the format represents these values.List.contains,List.elem, and every otherBEq-based search use this notion.=(DecidableEq) is structural equality of the stored interchange word: distinct signed-zero encodings are unequal and every NaN equals itself.decide (x = y),List.Nodup,Multiset, andFinsetuse this notion.Hashablehashes the same word, sox = yimplieshash x = hash y.
These instances do not provide LawfulBEq. Using configured values as Std.HashMap or
Std.HashSet keys requires an equality and hashing convention that satisfies their laws.
< and ≤ use IEEE numerical comparisons: a < b holds exactly when the numerical comparison
returns some .lt, and a ≤ b when it returns some .lt or some .eq. Every comparison
involving a NaN is false, so a ≤ a fails for NaN and these relations are not a Preorder.
max and min are IEEE maximum and minimum: they propagate NaN and order -0 below +0,
so max a b = if a ≤ b then b else a fails on NaN inputs.
Configured binary comparison follows the descriptor's IEEE-style numerical order.
NaNs are unordered, signed zeros compare equal, and every other pair is ordered by exact value.
The stored word determines the value, so decoding to the model is injective.
Comparison on configured values is comparison of their exact-width models.
Comparison against a NaN is unordered.
The default configured binary value is positive zero.
The default configured binary value is positive zero.
Structural equality of the stored interchange word.
This differs from ==: distinct signed-zero encodings are unequal and a NaN equals itself.
Deciding equality on the
exact-width model keeps the instance independent of the packed carrier.
Hash of the complete interchange word.
Structural equality = guarantees equal hashes. Numerical equality == alone does not,
since distinct signed-zero encodings compare numerically equal.
The hash of a configured binary value is the hash of its interchange word.
IEEE strict order: a < b holds when the numerical comparison returns some .lt.
IEEE weak order: a ≤ b holds when the comparison returns some .lt or some .eq.
< is decided by the executable comparison.
≤ is decided by the executable comparison.
IEEE maximum: NaN operands propagate as a quiet NaN and max (-0) (+0) = +0.
This is not the order-theoretic maximum of ≤, since NaNs are unordered by ≤.
IEEE minimum: NaN operands propagate as a quiet NaN and min (-0) (+0) = -0.
This is not the order-theoretic minimum of ≤, since NaNs are unordered by ≤.
max decodes to IEEE maximum on the exact-width models.
min decodes to IEEE minimum on the exact-width models.
< is the executable strict comparison.
≤ is the executable weak comparison.
< holds exactly when the model comparison returns some .lt.
< on configured values is Model.lt on their models.
≤ holds exactly when the model comparison returns some .lt or some .eq.
≤ on configured values is Model.le on their models.
≤ is < or numerical equality ==.
Nothing is strictly below or above a NaN.
Nothing is weakly below or above a NaN.
Strict order is irreflexive, for NaN because it is unordered and otherwise by equality.
≤ is reflexive exactly on non-NaN values.
Configured binary values print their mathematical value rather than their packed carrier.
Numeral literals are rounded once from the exact natural number into the destination format.
Scientific and decimal literals are rounded once from their exact rational value into the destination format.
Negation follows the destination format's signed-zero and exceptional-value policy.