fact: Definition toF x : float radix2 := match Prim2SF x with | S754_zero _ => Fzero | S754_infinity _ | S754_nan => Basic.Fnan | S754_finite s m e => Basic.Float s m e end.
imports: Coq(ZArith Reals) Int63Compat Coq(Floats Psatz) Flocq(Zaux Raux BinarySingleNaN PrimFloat Sterbenz Mult_error) Missing.Stdlib Missing.Flocq Xreal Basic Sig