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