		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-annotation-list

Pretty-print a list of annotations, one per line.

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

Definitions and Theorems

Function: pprint-annotation-list

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

Theorem: msg-listp-of-pprint-annotation-list

(defthm msg-listp-of-pprint-annotation-list
  (b* ((lines (pprint-annotation-list anns level)))
    (msg-listp lines))
  :rule-classes :rewrite)