Pretty-print a list of structure declarations.
(pprint-struct-declon-list members level) → lines
Function:
(defun pprint-struct-declon-list (members level) (declare (xargs :guard (and (struct-declon-listp members) (natp level)))) (let ((__function__ 'pprint-struct-declon-list)) (declare (ignorable __function__)) (cond ((endp members) nil) (t (cons (pprint-struct-declon (car members) level) (pprint-struct-declon-list (cdr members) level))))))
Theorem:
(defthm msg-listp-of-pprint-struct-declon-list (b* ((lines (pprint-struct-declon-list members level))) (msg-listp lines)) :rule-classes :rewrite)
Theorem:
(defthm pprint-struct-declon-list-of-struct-declon-list-fix-members (equal (pprint-struct-declon-list (struct-declon-list-fix members) level) (pprint-struct-declon-list members level)))
Theorem:
(defthm pprint-struct-declon-list-struct-declon-list-equiv-congruence-on-members (implies (struct-declon-list-equiv members members-equiv) (equal (pprint-struct-declon-list members level) (pprint-struct-declon-list members-equiv level))) :rule-classes :congruence)
Theorem:
(defthm pprint-struct-declon-list-of-nfix-level (equal (pprint-struct-declon-list members (nfix level)) (pprint-struct-declon-list members level)))
Theorem:
(defthm pprint-struct-declon-list-nat-equiv-congruence-on-level (implies (acl2::nat-equiv level level-equiv) (equal (pprint-struct-declon-list members level) (pprint-struct-declon-list members level-equiv))) :rule-classes :congruence)