fact: Definition SF2B' {prec emax} (x : spec_float) : binary_float prec emax := match x with | S754_zero s => B754_zero s | S754_infinity s => B754_infinity s | S754_nan => B754_nan | S754_finite s m e => match bounded prec emax m e as b return bounded prec emax m e = b -> _ with | true => B754_finite s m e | false => fun H => B754_nan end eq_refl end.
imports: Coq(ZArith SpecFloat) Flocq(BinarySingleNaN)