|
|
|---|
|
|
|
|---|
Check that a list of function definitions has no nested function definitions.
(fundef-list-nofunp x) → std::bool
This lifts fundef-nofunp to lists.
Analogously to fundef-nofunp,
the function definitions passed as argument to
Function:
(defun fundef-list-nofunp (x) (declare (xargs :guard (fundef-listp x))) (let ((__function__ 'fundef-list-nofunp)) (declare (ignorable __function__)) (if (consp x) (and (fundef-nofunp (car x)) (fundef-list-nofunp (cdr x))) t)))
Theorem:
(defthm fundef-list-nofunp-of-fundef-list-fix-x (equal (fundef-list-nofunp (fundef-list-fix x)) (fundef-list-nofunp x)))
Theorem:
(defthm fundef-list-nofunp-fundef-list-equiv-congruence-on-x (implies (fundef-list-equiv x x-equiv) (equal (fundef-list-nofunp x) (fundef-list-nofunp x-equiv))) :rule-classes :congruence)