		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jparam

Pretty-print a formal parameter.

Signature
(print-jparam param) → part
Arguments: param — Guard (jparamp param).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-jparam

(defun print-jparam (param)
  (declare (xargs :guard (jparamp param)))
  (let ((__function__ 'print-jparam))
    (declare (ignorable __function__))
    (b* (((jparam param) param))
      (msg "~@0~@1 ~@2"
           (if param.final? "final " "")
           (print-jtype param.type)
           param.name))))

Theorem: msgp-of-print-jparam

(defthm msgp-of-print-jparam
  (b* ((part (print-jparam param)))
    (msgp part))
  :rule-classes :rewrite)