		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-binop

Pretty-print a binary operator.

Signature
(pprint-binop op) → part
Arguments: op — Guard (binopp op).
Returns: part — Type (msgp part).

Definitions and Theorems

Function: pprint-binop

(defun pprint-binop (op)
  (declare (xargs :guard (binopp op)))
  (let ((__function__ 'pprint-binop))
    (declare (ignorable __function__))
    (binop-case op
                :mul "*"
                :div "/"
                :rem "%"
                :add "+"
                :sub "-"
                :shl "<<"
                :shr ">>"
                :lt "<"
                :gt ">"
                :le "<="
                :ge ">="
                :eq "=="
                :ne "!="
                :bitand "&"
                :bitxor "^"
                :bitior "|"
                :logand "&&"
                :logor "||"
                :asg "="
                :asg-mul "*="
                :asg-div "/="
                :asg-rem "%="
                :asg-add "+="
                :asg-sub "-="
                :asg-shl "<<="
                :asg-shr ">>="
                :asg-and "&="
                :asg-xor "^="
                :asg-ior "|=")))

Theorem: msgp-of-pprint-binop

(defthm msgp-of-pprint-binop
  (b* ((part (pprint-binop op)))
    (msgp part))
  :rule-classes :rewrite)

Theorem: pprint-binop-of-binop-fix-op

(defthm pprint-binop-of-binop-fix-op
  (equal (pprint-binop (binop-fix op))
         (pprint-binop op)))

Theorem: pprint-binop-binop-equiv-congruence-on-op

(defthm pprint-binop-binop-equiv-congruence-on-op
  (implies (binop-equiv op op-equiv)
           (equal (pprint-binop op)
                  (pprint-binop op-equiv)))
  :rule-classes :congruence)