Check if all the parameter declarations in a list have formal dynamic semantics.
(paramdecl-list-formalp paramdecls) → yes/no
Function:
(defun paramdecl-list-formalp (paramdecls) (declare (xargs :guard (paramdecl-listp paramdecls))) (declare (xargs :guard (paramdecl-list-unambp paramdecls))) (let ((__function__ 'paramdecl-list-formalp)) (declare (ignorable __function__)) (or (endp paramdecls) (and (paramdecl-formalp (car paramdecls)) (paramdecl-list-formalp (cdr paramdecls))))))
Theorem:
(defthm booleanp-of-paramdecl-list-formalp (b* ((yes/no (paramdecl-list-formalp paramdecls))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm paramdecl-list-formalp-of-paramdecl-list-fix-paramdecls (equal (paramdecl-list-formalp (paramdecl-list-fix paramdecls)) (paramdecl-list-formalp paramdecls)))
Theorem:
(defthm paramdecl-list-formalp-paramdecl-list-equiv-congruence-on-paramdecls (implies (paramdecl-list-equiv paramdecls paramdecls-equiv) (equal (paramdecl-list-formalp paramdecls) (paramdecl-list-formalp paramdecls-equiv))) :rule-classes :congruence)