		Search-engine friendly clone of the ACL2 documentation.

Atc-pretty-printer

Pprint-unop

Pretty-print a unary operator.

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

Definitions and Theorems

Function: pprint-unop

(defun pprint-unop (op)
  (declare (xargs :guard (unopp op)))
  (let ((__function__ 'pprint-unop))
    (declare (ignorable __function__))
    (unop-case op
               :address "&"
               :indir "*"
               :plus "+"
               :minus "-"
               :bitnot "~~"
               :lognot "!")))

Theorem: msgp-of-pprint-unop

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

Theorem: pprint-unop-of-unop-fix-op

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

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

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