		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-incexpr-p

Recognizer for pre/post increment/decrement and assignment expressions.

Signature
(vl-incexpr-p x) → bool
Arguments: x — Guard (vl-expr-p x).
Returns: bool — Type (booleanp bool).

Definitions and Theorems

Function: vl-incexpr-p

(defun vl-incexpr-p (x)
 (declare (xargs :guard (vl-expr-p x)))
 (let ((__function__ 'vl-incexpr-p))
  (declare (ignorable __function__))
  (vl-expr-case
      x
      :vl-unary (or (vl-unaryop-equiv x.op :vl-unary-preinc)
                    (vl-unaryop-equiv x.op :vl-unary-predec)
                    (vl-unaryop-equiv x.op :vl-unary-postinc)
                    (vl-unaryop-equiv x.op :vl-unary-postdec))
      :vl-binary (or (vl-binaryop-equiv x.op :vl-binary-assign)
                     (vl-binaryop-equiv x.op :vl-binary-plusassign)
                     (vl-binaryop-equiv x.op :vl-binary-minusassign)
                     (vl-binaryop-equiv x.op :vl-binary-timesassign)
                     (vl-binaryop-equiv x.op :vl-binary-divassign)
                     (vl-binaryop-equiv x.op :vl-binary-remassign)
                     (vl-binaryop-equiv x.op :vl-binary-andassign)
                     (vl-binaryop-equiv x.op :vl-binary-orassign)
                     (vl-binaryop-equiv x.op :vl-binary-xorassign)
                     (vl-binaryop-equiv x.op :vl-binary-shlassign)
                     (vl-binaryop-equiv x.op :vl-binary-shrassign)
                     (vl-binaryop-equiv x.op :vl-binary-ashlassign)
                     (vl-binaryop-equiv x.op :vl-binary-ashrassign))
      :otherwise nil)))

Theorem: booleanp-of-vl-incexpr-p

(defthm booleanp-of-vl-incexpr-p
  (b* ((bool (vl-incexpr-p x)))
    (booleanp bool))
  :rule-classes :type-prescription)

Theorem: vl-incexpr-p-of-vl-expr-fix-x

(defthm vl-incexpr-p-of-vl-expr-fix-x
  (equal (vl-incexpr-p (vl-expr-fix x))
         (vl-incexpr-p x)))

Theorem: vl-incexpr-p-vl-expr-equiv-congruence-on-x

(defthm vl-incexpr-p-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-incexpr-p x)
                  (vl-incexpr-p x-equiv)))
  :rule-classes :congruence)