		Search-engine friendly clone of the ACL2 documentation.

Input-pretty-printer

Pprint-input-item-list

Pretty-print a list of input items.

Signature
(pprint-input-item-list items level) → lines
Arguments: items — Guard (input-item-listp items).; level — Guard (natp level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-input-item-list

(defun pprint-input-item-list (items level)
  (declare (xargs :guard (and (input-item-listp items)
                              (natp level))))
  (let ((__function__ 'pprint-input-item-list))
    (declare (ignorable __function__))
    (cond ((endp items) nil)
          (t (cons (pprint-input-item (car items) level)
                   (pprint-input-item-list (cdr items)
                                           level))))))

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

(defthm msg-listp-of-pprint-input-item-list
  (b* ((lines (pprint-input-item-list items level)))
    (msg-listp lines))
  :rule-classes :rewrite)