fact: Definition binary_float_of_bits_aux x := let '(sx, mx, ex) := split_bits x in if Zeq_bool ex 0 then match mx with | Z0 => F754_zero sx | Zpos px => F754_finite sx px emin | Zneg _ => F754_nan false xH end else if Zeq_bool ex (Zpower 2 ew - 1) then match mx with | Z0 => F754_infinity sx | Zpos plx => F754_nan sx plx | Zneg _ => F754_nan false xH end else match (mx + Zpower 2 mw)%Z with | Zpos px => F754_finite sx px (ex + emin - 1) | _ => F754_nan false xH end.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary