Print a list of one or more declarations, one per line, all with the same indentation.
(print-decl-list decls pstate) → new-pstate
Function:
(defun print-decl-list (decls pstate) (declare (xargs :guard (and (decl-listp decls) (pristatep pstate)))) (declare (xargs :guard (and (consp decls) (decl-list-unambp decls)))) (let ((__function__ 'print-decl-list)) (declare (ignorable __function__)) (b* (((unless (mbt (consp decls))) (pristate-fix pstate)) (pstate (print-decl (car decls) pstate)) ((when (endp (cdr decls))) pstate)) (print-decl-list (cdr decls) pstate))))
Theorem:
(defthm pristatep-of-print-decl-list (b* ((new-pstate (print-decl-list decls pstate))) (pristatep new-pstate)) :rule-classes :rewrite)
Theorem:
(defthm print-decl-list-of-decl-list-fix-decls (equal (print-decl-list (decl-list-fix decls) pstate) (print-decl-list decls pstate)))
Theorem:
(defthm print-decl-list-decl-list-equiv-congruence-on-decls (implies (decl-list-equiv decls decls-equiv) (equal (print-decl-list decls pstate) (print-decl-list decls-equiv pstate))) :rule-classes :congruence)
Theorem:
(defthm print-decl-list-of-pristate-fix-pstate (equal (print-decl-list decls (pristate-fix pstate)) (print-decl-list decls pstate)))
Theorem:
(defthm print-decl-list-pristate-equiv-congruence-on-pstate (implies (pristate-equiv pstate pstate-equiv) (equal (print-decl-list decls pstate) (print-decl-list decls pstate-equiv))) :rule-classes :congruence)