		Search-engine friendly clone of the ACL2 documentation.

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
   :and "&&"
   :or "||"
   :eq "=="
   :ne "!="
   :ge ">="
   :gt ">"
   :le "<="
   :lt "<"
   :bitxor "^"
   :bitior "|"
   :bitand "&"
   :shl "<<"
   :shr ">>"
   :add "+"
   :sub "-"
   :mul "*"
   :div "/"
   :rem "%"
   :pow "**"
   :otherwise
   (prog2$
        (raise "op ~x0 should have been handled as an operator call"
               (binop-kind op))
        "ERROR"))))

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)