Library Coq.Floats.FloatLemmas


Require Import ZArith Int63 SpecFloat PrimFloat FloatOps FloatAxioms.
Require Import Psatz.

Support results involving frexp and ldexp


Lemma shift_value : shift = (2*emax + prec)%Z.

Theorem frexp_spec : forall f, let (m,e) := frexp f in (Prim2SF m, e) = SFfrexp prec emax (Prim2SF f).

Theorem ldexp_spec : forall f e, Prim2SF (ldexp f e) = SFldexp prec emax (Prim2SF f) e.