		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jimport

Pretty-print an import declaration.

Signature
(print-jimport import indent-level) → line
Arguments: import — Guard (jimportp import).; indent-level — Guard (natp indent-level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: print-jimport

(defun print-jimport (import indent-level)
  (declare (xargs :guard (and (jimportp import)
                              (natp indent-level))))
  (let ((__function__ 'print-jimport))
    (declare (ignorable __function__))
    (print-jline (msg "import ~s0~@1;"
                      (if (jimport->static? import)
                          "static "
                        "")
                      (jimport->target import))
                 indent-level)))

Theorem: msgp-of-print-jimport

(defthm msgp-of-print-jimport
  (b* ((line (print-jimport import indent-level)))
    (msgp line))
  :rule-classes :rewrite)