		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-obj-declon

Pretty-print an object declaration.

Signature
(pprint-obj-declon declon level options) → lines
Arguments: declon — Guard (obj-declonp declon).; level — Guard (natp level).; options — Guard (pprint-options-p options).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-obj-declon

(defun pprint-obj-declon (declon level options)
 (declare (xargs :guard (and (obj-declonp declon)
                             (natp level)
                             (pprint-options-p options))))
 (let ((__function__ 'pprint-obj-declon))
  (declare (ignorable __function__))
  (b* (((obj-declon declon) declon))
   (pprint-one-line
    (msg "~@0~@1 ~@2~@3;"
         (scspecseq-case declon.scspec
                         :none ""
                         :extern "extern ")
         (pprint-tyspecseq declon.tyspec)
         (pprint-obj-declor declon.declor)
         (if declon.init? (msg " = ~@0"
                               (pprint-initer declon.init? options))
           ""))
    (lnfix level)))))

Theorem: msg-listp-of-pprint-obj-declon

(defthm msg-listp-of-pprint-obj-declon
  (b* ((lines (pprint-obj-declon declon level options)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: pprint-obj-declon-of-obj-declon-fix-declon

(defthm pprint-obj-declon-of-obj-declon-fix-declon
  (equal (pprint-obj-declon (obj-declon-fix declon)
                            level options)
         (pprint-obj-declon declon level options)))

Theorem: pprint-obj-declon-obj-declon-equiv-congruence-on-declon

(defthm pprint-obj-declon-obj-declon-equiv-congruence-on-declon
  (implies (obj-declon-equiv declon declon-equiv)
           (equal (pprint-obj-declon declon level options)
                  (pprint-obj-declon declon-equiv level options)))
  :rule-classes :congruence)

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

(defthm pprint-obj-declon-of-nfix-level
  (equal (pprint-obj-declon declon (nfix level)
                            options)
         (pprint-obj-declon declon level options)))

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

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

Theorem: pprint-obj-declon-of-pprint-options-fix-options

(defthm pprint-obj-declon-of-pprint-options-fix-options
  (equal (pprint-obj-declon declon
                            level (pprint-options-fix options))
         (pprint-obj-declon declon level options)))

Theorem: pprint-obj-declon-pprint-options-equiv-congruence-on-options

(defthm pprint-obj-declon-pprint-options-equiv-congruence-on-options
  (implies (pprint-options-equiv options options-equiv)
           (equal (pprint-obj-declon declon level options)
                  (pprint-obj-declon declon level options-equiv)))
  :rule-classes :congruence)