fact: Fixpoint convert_expr (t : RExpr) : R := match t with | reUnknown x => nth (nat_of_P x) (R0 :: unknown_values) R0 | reInteger x => IZR x | reFloat2 x y => float2R (Float2 x y) | reFloat10 x y => float10R (Float10 x y) | reUnary o x => match o with | uoNeg => Ropp | uoSqrt => sqrt | uoAbs => Rabs | uoInv => Rinv end (convert_expr x) | reBinary o x y => match o with | boAdd => Rplus | boSub => Rminus | boMul => Rmult | boDiv => Rdiv end (convert_expr x) (convert_expr y) | reBpow2 x => bpow radix2 x | reBpow10 x => bpow radix10 x | rePow2 x => powerRZ 2%R x | rePow10 x => powerRZ 10%R x | reINR x => INR (nat_of_P x) | reIZR x => IZR x | reRound f m x => Generic_fmt.round radix2 (convert_exp f) (convert_mode m) (convert_expr x) end.
imports: Coq(ZArith Reals List Lia) Flocq(Core) Gappa_library