fact: Definition bits_of_binary_float (x : binary_float) := match x with | B754_zero sx => join_bits sx 0 0 | B754_infinity sx => join_bits sx 0 (Zpower 2 ew - 1) | B754_nan sx plx _ => join_bits sx (Zpos plx) (Zpower 2 ew - 1) | B754_finite sx mx ex _ => let m := (Zpos mx - Zpower 2 mw)%Z in if Zle_bool 0 m then join_bits sx m (ex - emin + 1) else join_bits sx (Zpos mx) 0 end.
imports: Coq(ZArith Reals Lia SpecFloat) Core BinarySingleNaN Binary