		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jresult

Pretty-print a method result.

Signature
(print-jresult result) → part
Arguments: result — Guard (jresultp result).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-jresult

(defun print-jresult (result)
  (declare (xargs :guard (jresultp result)))
  (let ((__function__ 'print-jresult))
    (declare (ignorable __function__))
    (jresult-case result
                  :type (print-jtype result.get)
                  :void "void")))

Theorem: msgp-of-print-jresult

(defthm msgp-of-print-jresult
  (b* ((part (print-jresult result)))
    (msgp part))
  :rule-classes :rewrite)