Pretty-print a list of external declarations.
(pprint-ext-declon-list exts options) → lines
We print a blank line before each one.
Function:
(defun pprint-ext-declon-list (exts options) (declare (xargs :guard (and (ext-declon-listp exts) (pprint-options-p options)))) (let ((__function__ 'pprint-ext-declon-list)) (declare (ignorable __function__)) (cond ((endp exts) nil) (t (append (pprint-one-line-blank) (pprint-ext-declon (car exts) options) (pprint-ext-declon-list (cdr exts) options))))))
Theorem:
(defthm msg-listp-of-pprint-ext-declon-list (b* ((lines (pprint-ext-declon-list exts options))) (msg-listp lines)) :rule-classes :rewrite)