fact: Definition SFnearbyint_binary m sx mx ex := if (0 <=? ex)%Z then S754_finite sx mx ex else let mx'' := SFnearbyint_binary_aux m sx mx ex in match mx'' with | Z.pos n => let (mx''', ex''') := shl_align_fexp n 0 in S754_finite sx mx''' ex''' | Z.neg n => S754_nan | Z0 => S754_zero sx end.
imports: Coq(ZArith Reals Psatz SpecFloat) Core Round Bracket Operations Div Sqrt Relative