		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-topdecl

Pretty-print a top-level declaration.

Signature
(pprint-topdecl decl) → lines
Arguments: decl — Guard (topdeclp decl).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-topdecl

(defun pprint-topdecl (decl)
  (declare (xargs :guard (topdeclp decl)))
  (let ((__function__ 'pprint-topdecl))
    (declare (ignorable __function__))
    (topdecl-case decl
                  :function (pprint-fundecl decl.get 1)
                  :struct (pprint-structdecl decl.get 1)
                  :mapping (pprint-mappingdecl decl.get 1))))

Theorem: msg-listp-of-pprint-topdecl

(defthm msg-listp-of-pprint-topdecl
  (b* ((lines (pprint-topdecl decl)))
    (msg-listp lines))
  :rule-classes :rewrite)