fact: Definition Prim2SF f := if is_nan f then S754_nan else if is_zero f then S754_zero (get_sign f) else if is_infinity f then S754_infinity (get_sign f) else let (r, exp) := Z.frexp f in let e := (exp - prec)%Z in let (shr, e') := shr_fexp prec emax (φ (normfr_mantissa r))%uint63 e loc_Exact in match shr_m shr with | Zpos p => S754_finite (get_sign f) p e' | Zneg _ | Z0 => S754_zero false end.
imports: ZArith Uint63 SpecFloat PrimFloat