Print a list of zero or more external declarations.
(print-extdecl-list extdecls pstate) → new-pstate
We separate them with blank lines.
Function:
(defun print-extdecl-list (extdecls pstate) (declare (xargs :guard (and (extdecl-listp extdecls) (pristatep pstate)))) (declare (xargs :guard (extdecl-list-unambp extdecls))) (let ((__function__ 'print-extdecl-list)) (declare (ignorable __function__)) (b* (((when (endp extdecls)) (pristate-fix pstate)) (pstate (print-extdecl (car extdecls) pstate))) (print-extdecl-list (cdr extdecls) pstate))))
Theorem:
(defthm pristatep-of-print-extdecl-list (b* ((new-pstate (print-extdecl-list extdecls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-extdecl-list-of-extdecl-list-fix-extdecls (equal (print-extdecl-list (extdecl-list-fix extdecls) pstate) (print-extdecl-list extdecls pstate)))
Theorem:
(defthm print-extdecl-list-extdecl-list-equiv-congruence-on-extdecls (implies (extdecl-list-equiv extdecls extdecls-equiv) (equal (print-extdecl-list extdecls pstate) (print-extdecl-list extdecls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-extdecl-list-of-pristate-fix-pstate (equal (print-extdecl-list extdecls (pristate-fix pstate)) (print-extdecl-list extdecls pstate)))
Theorem:
(defthm print-extdecl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-extdecl-list extdecls pstate) (print-extdecl-list extdecls pstate-equiv))) :rule-classes :congruence)