fact: Definition Fround_at_prec {beta} mode prec (uf : ufloat beta) : float beta := match uf with | Unan => Fnan | Uzero => Fzero | Ufloat sign m1 e1 pos => match (Zpos (count_digits beta m1) - Zpos prec)%Z with | Zpos nb => let d := shift beta xH nb in match Z.div_eucl (Zpos m1) (Zpos d) with | (Zpos m2, r) => let pos2 := adjust_pos r d pos in let e2 := (e1 + Zpos nb)%Z in Float sign (adjust_mantissa mode m2 pos2 sign) e2 | _ => Fnan end | Z0 => Float sign (adjust_mantissa mode m1 pos sign) e1 | _ => Float sign m1 e1 end end.
imports: Coq(Reals Bool ZArith) Flocq(Zaux Raux Div Sqrt) Xreal Basic