		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-junop

Pretty-print a unary operator.

Signature
(print-junop unop) → part
Arguments: unop — Guard (junopp unop).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-junop

(defun print-junop (unop)
  (declare (xargs :guard (junopp unop)))
  (let ((__function__ 'print-junop))
    (declare (ignorable __function__))
    (junop-case unop
                :preinc "++"
                :predec "--"
                :uplus "+"
                :uminus "-"
                :bitcompl "~~"
                :logcompl "!")))

Theorem: msgp-of-print-junop

(defthm msgp-of-print-junop
  (b* ((part (print-junop unop)))
    (msgp part))
  :rule-classes :rewrite)