		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-section-list

Pretty-print a list of input sections.

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

Definitions and Theorems

Function: pprint-input-section-list

(defun pprint-input-section-list (insecs)
  (declare (xargs :guard (input-section-listp insecs)))
  (let ((__function__ 'pprint-input-section-list))
    (declare (ignorable __function__))
    (cond ((endp insecs) nil)
          (t (append (pprint-input-section (car insecs))
                     (pprint-input-section-list (cdr insecs)))))))

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

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