fact: Definition Bfma m (x y z: binary_float) := match x, y with | B754_nan, _ | _, B754_nan | B754_infinity _, B754_zero _ | B754_zero _, B754_infinity _ => B754_nan | B754_infinity sx, B754_infinity sy | B754_infinity sx, B754_finite sy _ _ _ | B754_finite sx _ _ _, B754_infinity sy => let s := xorb sx sy in match z with | B754_nan => B754_nan | B754_infinity sz => if Bool.eqb s sz then z else B754_nan | _ => B754_infinity s end | B754_finite sx _ _ _, B754_zero sy | B754_zero sx, B754_finite sy _ _ _ | B754_zero sx, B754_zero sy => match z with | B754_nan => B754_nan | B754_zero _ => B754_zero (Bfma_szero m x y z) | _ => z end | B754_finite sx mx ex _, B754_finite sy my ey _ => match z with | B754_nan => B754_nan | B754_infinity sz => z | B754_zero _ => let X := Float radix2 (cond_Zopp sx (Zpos mx)) ex in let Y := Float radix2 (cond_Zopp sy (Zpos my)) ey in let '(Float _ mr er) := Fmult X Y in binary_normalize m mr er (Bfma_szero m x y z) | B754_finite sz mz ez _ => let X := Float radix2 (cond_Zopp sx (Zpos mx)) ex in let Y := Float radix2 (cond_Zopp sy (Zpos my)) ey in let Z := Float radix2 (cond_Zopp sz (Zpos mz)) ez in let '(Float _ mr er) := Fplus (Fmult X Y) Z in binary_normalize m mr er (Bfma_szero m x y z) end end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative