fact: Definition binary_round_aux sx mx ex lx := let '(mrs', e') := shr_fexp mx ex lx in let '(mrs'', e'') := shr_fexp (round_nearest_even (shr_m mrs') (loc_of_shr_record mrs')) e' loc_Exact in match shr_m mrs'' with | Z0 => S754_zero sx | Zpos m => if Zle_bool e'' (emax - prec) then S754_finite sx m e'' else S754_infinity sx | _ => S754_nan end.
imports: ZArith FloatClass