fact: Definition AtomToProp g l := match g with | InInt32 t => - IZR (Int32.N / 2) <= evalCArithExpr2 t l <= IZR (Int32.N / 2 - 1) | InInt51 t => -2251799813685248 <= evalCArithExpr2 t l <= 2251799813685247 | InInt64 t => - IZR (Int64.N / 2) <= evalCArithExpr2 t l <= IZR (Int64.N / 2 - 1) | InFloat64 t => Rabs (evalCArithExpr2 t l) <= Rrnd.maxval | InFloat64Int t => Rabs (evalCArithExpr2 t l) <= Rpow2 53 | NonZero t => evalCArithExpr2 t l <> 0 | NonNeg t => 0 <= evalCArithExpr2 t l | RndExact md t => let u := evalCArithExpr2 t l in round radix2 (FLT_exp emin prec) (round_mode md) u = u | LdexpControl n t p => Rabs (evalCArithExpr2 t l) <= IZR (radix2 ^ Rrnd.prec - 1) * Rpow2 (n - Rrnd.prec) /\ IZR n + evalCArithExpr2 p l <= IZR Rrnd.emax end.
imports: Coq(Bool Floats Reals List Lia Lra) Flocq(Core PrimFloat BinarySingleNaN Operations) Specific_bigint Specific_ops Interval_helper Float_full Prog Lang_expr