		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-stmt

Pretty-print a statement.

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

Note that we print the block items that form a compound statement one after the other, without surrounding curly braces. We print those curly braces when printing the surrounding statements.

For simplicity, and perhaps for good style, we always print curly braces around certain sub-statements (e.g. of if).

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

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

Theorem: return-type-of-pprint-block-item.lines

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

Theorem: return-type-of-pprint-block-item-list.lines

(defthm return-type-of-pprint-block-item-list.lines
  (b* ((?lines (pprint-block-item-list items level options)))
    (msg-listp lines))
  :rule-classes :rewrite)

Subtopics

Pprint-block-item-list
Pprint-block-item