fact: Definition SF2Prim ef := match ef with | S754_nan => nan | S754_zero false => zero | S754_zero true => neg_zero | S754_infinity false => infinity | S754_infinity true => neg_infinity | S754_finite s m e => let pm := of_uint63 (of_Z (Zpos m)) in let f := Z.ldexp pm e in if s then (-f)%float else f end.
imports: ZArith Uint63 SpecFloat PrimFloat