fact: Definition fromZ_DN (p : precision) x := match x with | Z0 => zero | Zpos x => match (x ?= 9007199254740992)%positive with | Lt => of_int63 (Int63.of_pos x) | _ => let x := Zpos x in let d := Z.log2 x in let e := (d - 52)%Z in let m := Z.shiftr x e in next_down (Z.ldexp (of_int63 (of_Z m)) e) end | Zneg x => match (x ?= 9007199254740992)%positive with | Lt => (-(of_int63 (Int63.of_pos x)))%float | _ => let x := Zpos x in let d := Z.log2 x in let e := (d - 52)%Z in let m := Z.shiftr x e in Z.ldexp (-(of_int63 (Int63.of_Z m + 1))) e end end.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig