		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-section

Pretty-print an input section.

Signature
(pprint-input-section insec) → lines
Arguments: insec — Guard (input-sectionp insec).
Returns: lines — Type (msg-listp lines).

Add a blank line at the end.

Definitions and Theorems

Function: pprint-input-section

(defun pprint-input-section (insec)
  (declare (xargs :guard (input-sectionp insec)))
  (let ((__function__ 'pprint-input-section))
    (declare (ignorable __function__))
    (b* (((input-section insec) insec)
         (first (pprint-input-title insec.title 0))
         (rest (pprint-input-item-list insec.items 0)))
      (append (list first)
              rest (list (pprint-line-blank))))))

Theorem: msg-listp-of-pprint-input-section

(defthm msg-listp-of-pprint-input-section
  (b* ((lines (pprint-input-section insec)))
    (msg-listp lines))
  :rule-classes :rewrite)