		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-importdecl-list

Pretty-print a list of import-level declarations.

Signature
(pprint-importdecl-list decls) → lines
Arguments: decls — Guard (importdecl-listp decls).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: pprint-importdecl-list

(defun pprint-importdecl-list (decls)
 (declare (xargs :guard (importdecl-listp decls)))
 (let ((__function__ 'pprint-importdecl-list))
   (declare (ignorable __function__))
   (cond ((endp decls) nil)
         ((endp (cdr decls))
          (list (pprint-importdecl (car decls))))
         (t (cons (pprint-importdecl (car decls))
                  (append (list (pprint-line-blank))
                          (pprint-importdecl-list (cdr decls))))))))

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

(defthm msg-listp-of-pprint-importdecl-list
  (b* ((lines (pprint-importdecl-list decls)))
    (msg-listp lines))
  :rule-classes :rewrite)