|
|
|---|
|
|
|
|---|
Check that a function environment has no function definitions in the functions' bodies.
(funenv-nofunp x) → std::bool
We check each scope in the environment.
Function:
(defun funenv-nofunp (x) (declare (xargs :guard (funenvp x))) (let ((__function__ 'funenv-nofunp)) (declare (ignorable __function__)) (if (consp x) (and (funscope-nofunp (car x)) (funenv-nofunp (cdr x))) t)))
Theorem:
(defthm funenv-nofunp-of-funenv-fix-x (equal (funenv-nofunp (funenv-fix x)) (funenv-nofunp x)))
Theorem:
(defthm funenv-nofunp-funenv-equiv-congruence-on-x (implies (funenv-equiv x x-equiv) (equal (funenv-nofunp x) (funenv-nofunp x-equiv))) :rule-classes :congruence)