		Search-engine friendly clone of the ACL2 documentation.

Output-pretty-printer

Pprint-output-section

Pretty-print an output section.

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

Add a blank line at the end.

Definitions and Theorems

Function: pprint-output-section

(defun pprint-output-section (outsec)
  (declare (xargs :guard (output-sectionp outsec)))
  (let ((__function__ 'pprint-output-section))
    (declare (ignorable __function__))
    (b* (((output-section outsec) outsec)
         (title (pprint-output-title 0))
         (item (pprint-output-item outsec.item 0)))
      (append (list title)
              (list item)
              (list (pprint-line-blank))))))

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

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

Theorem: pprint-output-section-of-output-section-fix-outsec

(defthm pprint-output-section-of-output-section-fix-outsec
  (equal (pprint-output-section (output-section-fix outsec))
         (pprint-output-section outsec)))

Theorem: pprint-output-section-output-section-equiv-congruence-on-outsec

(defthm
    pprint-output-section-output-section-equiv-congruence-on-outsec
  (implies (output-section-equiv outsec outsec-equiv)
           (equal (pprint-output-section outsec)
                  (pprint-output-section outsec-equiv)))
  :rule-classes :congruence)