fact: Definition SFadd x y := match x, y with | S754_nan, _ | _, S754_nan => S754_nan | S754_infinity sx, S754_infinity sy => if Bool.eqb sx sy then x else S754_nan | S754_infinity _, _ => x | _, S754_infinity _ => y | S754_zero sx, S754_zero sy => if Bool.eqb sx sy then x else S754_zero false | S754_zero _, _ => y | _, S754_zero _ => x | S754_finite sx mx ex, S754_finite sy my ey => let ez := Z.min ex ey in binary_normalize (Zplus (cond_Zopp sx (Zpos (fst (shl_align mx ex ez)))) (cond_Zopp sy (Zpos (fst (shl_align my ey ez))))) ez false end.
imports: ZArith FloatClass