		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jaccess

Pretty-print an access modifier.

Signature
(print-jaccess access) → part
Arguments: access — Guard (jaccessp access).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-jaccess

(defun print-jaccess (access)
  (declare (xargs :guard (jaccessp access)))
  (let ((__function__ 'print-jaccess))
    (declare (ignorable __function__))
    (jaccess-case access
                  :public "public "
                  :protected "protected "
                  :private "private "
                  :default "")))

Theorem: msgp-of-print-jaccess

(defthm msgp-of-print-jaccess
  (b* ((part (print-jaccess access)))
    (msgp part))
  :rule-classes :rewrite)