fact: Definition operations prec deg xi := Build_operations (fun _ => TM.dummy) TM.dummy (fun o => match o with | Neg => TM.opp (prec, deg) xi | Abs => TM.abs (prec, deg) xi | Inv => TM.inv (prec, deg) xi | Sqr => TM.sqr (prec, deg) xi | Sqrt => TM.sqrt (prec, deg) xi | Cos => TM.cos (prec, deg) xi | Sin => TM.sin (prec, deg) xi | Tan => TM.tan (prec, deg) xi | Atan => TM.atan (prec, deg) xi | Exp => TM.exp (prec, deg) xi | Ln => TM.ln (prec, deg) xi | PowerInt n => TM.power_int n (prec, deg) xi | Nearbyint m => TM.nearbyint m (prec, deg) xi | RoundFlt m emin p => TM.round_flt (prec, deg) m emin p xi | ErrorFlt m emin p => TM.error_flt (prec, deg) m emin p xi | RoundFix m emin => TM.round_fix (prec, deg) m emin xi | ErrorFix m emin => TM.error_fix (prec, deg) m emin xi end) (fun o => match o with | Add => TM.add (prec, deg) xi | Sub => TM.sub (prec, deg) xi | Mul => TM.mul (prec, deg) xi | Div => TM.div (prec, deg) xi end) (fun _ => Xund) .
imports: Coq(Bool Reals) Flocq(Zaux Raux) Coq(List) Coquelicot(Coquelicot) mathcomp.ssreflect(ssreflect) Stdlib Coquelicot Xreal Xreal_derive Basic Interval Interval_compl Taylor_model Tree Prog