		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Unop-nonpointerp

Check if a unary operator does not involve pointers.

Signature
(unop-nonpointerp op) → yes/no
Arguments: op — Guard (unopp op).
Returns: yes/no — Type (booleanp yes/no).

These are unary plus, unary minus, and bitwise/logical negation/complement. The other two, address and indirection, involve pointers.

Definitions and Theorems

Function: unop-nonpointerp

(defun unop-nonpointerp (op)
  (declare (xargs :guard (unopp op)))
  (let ((__function__ 'unop-nonpointerp))
    (declare (ignorable __function__))
    (and (member-eq (unop-kind op)
                    '(:plus :minus :bitnot :lognot))
         t)))

Theorem: booleanp-of-unop-nonpointerp

(defthm booleanp-of-unop-nonpointerp
  (b* ((yes/no (unop-nonpointerp op)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: unop-nonpointerp-of-unop-fix-op

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

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

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