		Search-engine friendly clone of the ACL2 documentation.

Pretty-printer

Pprint-topdecl-list

Pretty-print a list of top-level declarations.

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

Definitions and Theorems

Function: pprint-topdecl-list

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

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

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