fact: Definition Fround_at_exp {beta} mode e2 (uf : ufloat beta) : float beta := match uf with | Unan => Fnan | Uzero => Fzero | Ufloat sign m1 e1 pos => match (e2 - e1)%Z with | Zpos nb => match Z.compare (Zpos (count_digits beta m1)) (Zpos nb) with | Gt => 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 Float sign (adjust_mantissa mode m2 pos2 sign) e2 | _ => Fnan end | Eq => let d := shift beta xH nb in let pos2 := adjust_pos (Zpos m1) d pos in if need_change_zero mode pos2 sign then Float sign xH e2 else Fzero | Lt => if need_change_zero mode pos_Lo sign then Float sign xH e2 else Fzero 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