		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jlocvar

Pretty-print a local variable declaration.

Signature
(print-jlocvar locvar indent-level) → line
Arguments: locvar — Guard (jlocvarp locvar).; indent-level — Guard (natp indent-level).
Returns: line — Type (msgp line).

Definitions and Theorems

Function: print-jlocvar

(defun print-jlocvar (locvar indent-level)
 (declare (xargs :guard (and (jlocvarp locvar)
                             (natp indent-level))))
 (let ((__function__ 'print-jlocvar))
  (declare (ignorable __function__))
  (b* (((jlocvar locvar) locvar))
   (if locvar.init?
       (print-jline
            (msg "~@0~@1 ~@2 = ~@3;"
                 (if locvar.final? "final " "")
                 (print-jtype locvar.type)
                 locvar.name
                 (print-jexpr locvar.init? (jexpr-rank-expression)))
            indent-level)
     (print-jline (msg "~@0~@1 ~@2;"
                       (if locvar.final? "final " "")
                       (print-jtype locvar.type)
                       locvar.name)
                  indent-level)))))

Theorem: msgp-of-print-jlocvar

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