		Search-engine friendly clone of the ACL2 documentation.

Atj-java-pretty-printer

Print-jbinop

Pretty-print a binary operator.

Signature
(print-jbinop binop) → part
Arguments: binop — Guard (jbinopp binop).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: print-jbinop

(defun print-jbinop (binop)
  (declare (xargs :guard (jbinopp binop)))
  (let ((__function__ 'print-jbinop))
    (declare (ignorable __function__))
    (jbinop-case binop
                 :mul "*"
                 :div "/"
                 :rem "%"
                 :add "+"
                 :sub "-"
                 :shl "<<"
                 :sshr ">>"
                 :ushr ">>>"
                 :lt "<"
                 :gt ">"
                 :le "<="
                 :ge ">="
                 :eq "=="
                 :ne "!="
                 :and "&"
                 :xor "^"
                 :ior "|"
                 :condand "&&"
                 :condor "||"
                 :asg "="
                 :asg-mul "*="
                 :asg-div "/="
                 :asg-rem "%="
                 :asg-add "+="
                 :asg-sub "-="
                 :asg-shl "<<="
                 :asg-sshr ">>="
                 :asg-ushr ">>>="
                 :asg-and "&="
                 :asg-xor "^="
                 :asg-ior "|=")))

Theorem: msgp-of-print-jbinop

(defthm msgp-of-print-jbinop
  (b* ((part (print-jbinop binop)))
    (msgp part))
  :rule-classes :rewrite)