fact: Fixpoint eval (e : expr) (l : list R) := match e with | Evar n => nth n l 0%R | Econst o => nullary_real o | Eunary o e1 => unary_real o (eval e1 l) | Ebinary o e1 e2 => binary_real o (eval e1 l) (eval e2 l) end.
imports: Coq(Reals List) Xreal Basic Interval