		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-compdecl

Pretty-print a struct component declaration.

Signature
(pprint-compdecl decl) → part
Arguments: decl — Guard (compdeclp decl).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-compdecl

(defun pprint-compdecl (decl)
  (declare (xargs :guard (compdeclp decl)))
  (let ((__function__ 'pprint-compdecl))
    (declare (ignorable __function__))
    (msg "~@0: ~@1"
         (pprint-identifier (compdecl->name decl))
         (pprint-type (compdecl->type decl)))))

Theorem: msgp-of-pprint-compdecl

(defthm msgp-of-pprint-compdecl
  (b* ((part (pprint-compdecl decl)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-compdecl-of-compdecl-fix-decl

(defthm pprint-compdecl-of-compdecl-fix-decl
  (equal (pprint-compdecl (compdecl-fix decl))
         (pprint-compdecl decl)))

Theorem: pprint-compdecl-compdecl-equiv-congruence-on-decl

(defthm pprint-compdecl-compdecl-equiv-congruence-on-decl
  (implies (compdecl-equiv decl decl-equiv)
           (equal (pprint-compdecl decl)
                  (pprint-compdecl decl-equiv)))
  :rule-classes :congruence)