fused multiply-add a x b + c with ONE rounding, as SM86's FFMA performs it:
the exact product (scale 2^300) and the exact addend (scale 2^150, raised to
2^300) are summed as signed exact magnitudes and rounded once. Special
values: any NaN operand quiets; inf x 0 is invalid; an infinite product or
addend with a finite partner gives that infinity; opposite infinities are
invalid. A zero exact sum carries the sign the sum rule gives (+0 unless
both are negative zero).
209def modelSignedScale =
210 (lambda unrestricted value : (family ModelSigned) . (lambda unrestricted factor : Nat .
211 (eliminate ModelSigned (lambda unrestricted current : (family ModelSigned) . (family ModelSigned)) value
212 (branch ModelSignedOf sign magnitude .
213 (constructor ModelSigned ModelSignedOf sign (nat-multiply magnitude factor))))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.