		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-structdecl

Pretty-print a struct declaration.

Signature
(pprint-structdecl decl level) → lines
Arguments: decl — Guard (structdeclp decl).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-structdecl

(defun pprint-structdecl (decl level)
 (declare (xargs :guard (and (structdeclp decl) (natp level))))
 (let ((__function__ 'pprint-structdecl))
  (declare (ignorable __function__))
  (b* (((structdecl decl) decl))
    (append
         (list (pprint-line (msg "~s0 ~@1 {"
                                 (if decl.recordp "record" "struct")
                                 (pprint-identifier decl.name))
                            level))
         (pprint-compdecl-list decl.components (1+ level))
         (list (pprint-line "}" level))))))

Theorem: msg-listp-of-pprint-structdecl

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