fact: Fixpoint FEeval (l : list R) (pe : FExpr) {struct pe} : R := match pe with | FEO => rO | FEI => rI | FEc c => phi c | FEX x => BinList.nth 0 x l | FEadd x y => FEeval l x + FEeval l y | FEsub x y => FEeval l x - FEeval l y | FEmul x y => FEeval l x * FEeval l y | FEopp x => - FEeval l x | FEinv x => / FEeval l x | FEdiv x y => FEeval l x / FEeval l y | FEpow x n => rpow (FEeval l x) (Cp_phi n) end.
imports: ZArith_base