		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-struct-declon-list

Pretty-print a list of structure declarations.

Signature
(pprint-struct-declon-list members level) → lines
Arguments: members — Guard (struct-declon-listp members).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-struct-declon-list

(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: msg-listp-of-pprint-struct-declon-list

(defthm msg-listp-of-pprint-struct-declon-list
  (b* ((lines (pprint-struct-declon-list members level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: pprint-struct-declon-list-of-struct-declon-list-fix-members

(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: pprint-struct-declon-list-struct-declon-list-equiv-congruence-on-members

(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: pprint-struct-declon-list-of-nfix-level

(defthm pprint-struct-declon-list-of-nfix-level
  (equal (pprint-struct-declon-list members (nfix level))
         (pprint-struct-declon-list members level)))

Theorem: pprint-struct-declon-list-nat-equiv-congruence-on-level

(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)