		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-struct-declon

Pretty-print a structure declaration.

Signature
(pprint-struct-declon member level) → line
Arguments: member — Guard (struct-declonp member).; level — Guard (natp level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: pprint-struct-declon

(defun pprint-struct-declon (member level)
  (declare (xargs :guard (and (struct-declonp member)
                              (natp level))))
  (let ((__function__ 'pprint-struct-declon))
    (declare (ignorable __function__))
    (b* (((struct-declon member) member))
      (pprint-line (msg "~@0 ~@1;"
                        (pprint-tyspecseq member.tyspec)
                        (pprint-obj-declor member.declor))
                   (lnfix level)))))

Theorem: msgp-of-pprint-struct-declon

(defthm msgp-of-pprint-struct-declon
  (b* ((line (pprint-struct-declon member level)))
    (msgp line))
  :rule-classes :rewrite)

Theorem: pprint-struct-declon-of-struct-declon-fix-member

(defthm pprint-struct-declon-of-struct-declon-fix-member
  (equal (pprint-struct-declon (struct-declon-fix member)
                               level)
         (pprint-struct-declon member level)))

Theorem: pprint-struct-declon-struct-declon-equiv-congruence-on-member

(defthm
      pprint-struct-declon-struct-declon-equiv-congruence-on-member
  (implies (struct-declon-equiv member member-equiv)
           (equal (pprint-struct-declon member level)
                  (pprint-struct-declon member-equiv level)))
  :rule-classes :congruence)

Theorem: pprint-struct-declon-of-nfix-level

(defthm pprint-struct-declon-of-nfix-level
  (equal (pprint-struct-declon member (nfix level))
         (pprint-struct-declon member level)))

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

(defthm pprint-struct-declon-nat-equiv-congruence-on-level
  (implies (acl2::nat-equiv level level-equiv)
           (equal (pprint-struct-declon member level)
                  (pprint-struct-declon member level-equiv)))
  :rule-classes :congruence)