fact: Fixpoint is_const (e : expr) n : bool := match e with | Var v => negb (ssrnat.eqn v n) | AppExt k f le => foldr (fun v acc => andb (is_const v n) acc) true le | AppExtD k f p le => false | App f e => andb (is_const f (S n)) (is_const e n) | Subst f e => andb (orb (ssrnat.eqn n 0) (is_const f n)) (is_const e n) | Cst _ => true | Binary b e1 e2 => andb (is_const e1 n) (is_const e2 n) | Unary u e => is_const e n | Int f e1 e2 => andb (is_const f (S n)) (andb (is_const e1 n) (is_const e2 n)) end.
imports: Coq(Reals Datatypes ssreflect ssrbool) mathcomp(seq) Rcomplements Hierarchy Derive RInt RInt_analysis Derive_2d Continuity ElemFct