fact: Fixpoint eval_bnd (prec : I.precision) (e : expr) := match e with | Evar _ => I.nai | Econst o => nullary_bnd prec o | Eunary o e1 => unary_bnd prec o (eval_bnd prec e1) | Ebinary o e1 e2 => binary_bnd prec o (eval_bnd prec e1) (eval_bnd prec e2) end.
imports: Coq(Reals List) Xreal Basic Interval