fact: Definition float_ulp (p : positive) (d m e : Z) := match m with | Zpos n => FLT_exp d (Zpos p) (e + Zpos (digits n))%Z | Zneg n => FLT_exp d (Zpos p) (e + Zpos (digits n))%Z | Z0 => d end.
imports: Coq(Bool ZArith Reals Lia) Flocq(Core Digits Round Relative) Gappa_definitions Gappa_dyadic Gappa_pred_bnd Gappa_round_def Gappa_round_aux Gappa_round