		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-importdecl

Pretty-print an import declaration.

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

Definitions and Theorems

Function: pprint-importdecl

(defun pprint-importdecl (decl)
  (declare (xargs :guard (importdeclp decl)))
  (let ((__function__ 'pprint-importdecl))
    (declare (ignorable __function__))
    (msg "import ~@0;"
         (pprint-programid (importdecl->program decl)))))

Theorem: msgp-of-pprint-importdecl

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

Theorem: pprint-importdecl-of-importdecl-fix-decl

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

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

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