		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jimports

Pretty-print a sequence of import declarations.

Signature
(print-jimports imports indent-level) → lines
Arguments: imports — Guard (jimport-listp imports).; indent-level — Guard (natp indent-level).
Returns: lines — Type (msg-listp lines).

Definitions and Theorems

Function: print-jimports

(defun print-jimports (imports indent-level)
  (declare (xargs :guard (and (jimport-listp imports)
                              (natp indent-level))))
  (let ((__function__ 'print-jimports))
    (declare (ignorable __function__))
    (cond ((endp imports) nil)
          (t (cons (print-jimport (car imports)
                                  indent-level)
                   (print-jimports (cdr imports)
                                   indent-level))))))

Theorem: msg-listp-of-print-jimports

(defthm msg-listp-of-print-jimports
  (b* ((lines (print-jimports imports indent-level)))
    (msg-listp lines))
  :rule-classes :rewrite)