fact: Fixpoint eval_Psatz (l : list NFormula) (e : Psatz) {struct e} : option NFormula := match e with | PsatzLet p1 p2 => match eval_Psatz l p1 with | None => None | Some f => eval_Psatz (f::l) p2 end | PsatzIn n => Some (nth n l (Pc cO, Equal)) | PsatzSquare e => Some (Psquare cO cI cplus ctimes ceqb e , NonStrict) | PsatzMulC re e => map_option (pexpr_times_nformula re) (eval_Psatz l e) | PsatzMulE f1 f2 => map_option2 nformula_times_nformula (eval_Psatz l f1) (eval_Psatz l f2) | PsatzAdd f1 f2 => map_option2 nformula_plus_nformula (eval_Psatz l f1) (eval_Psatz l f2) | PsatzC c => if cltb cO c then Some (Pc c, Strict) else None | PsatzZ => Some (Pc cO, Equal) end.
imports: NArith Relation_Definitions Setoid Env EnvRing List Bool OrderedRing Refl