		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-statement

Pretty-print a statement.

Signature
(pprint-statement stmt level) → lines
Arguments: stmt — Guard (statementp stmt).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Theorem: return-type-of-pprint-statement.lines

(defthm return-type-of-pprint-statement.lines
  (b* ((?lines (pprint-statement stmt level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-pprint-statement-list.lines

(defthm return-type-of-pprint-statement-list.lines
  (b* ((?lines (pprint-statement-list stmts level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-pprint-branch.lines

(defthm return-type-of-pprint-branch.lines
  (b* ((?lines (pprint-branch branch level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Theorem: return-type-of-pprint-branch-list.lines

(defthm return-type-of-pprint-branch-list.lines
  (b* ((?lines (pprint-branch-list branches level)))
    (msg-listp lines))
  :rule-classes :rewrite)

Subtopics

Pprint-statement-list
Pprint-branch-list
Pprint-branch