Recognizer for post increment/decrement operators.
Note that we treat all assignment operators as if they were
pre-increment operations, because they should "return" the updated value,
i.e.,
Function:
(defun vl-incexpr-post-p$inline (x) (declare (xargs :guard (vl-expr-p x))) (declare (xargs :guard (vl-incexpr-p x))) (let ((__function__ 'vl-incexpr-post-p)) (declare (ignorable __function__)) (vl-expr-case x :vl-unary (or (vl-unaryop-equiv x.op :vl-unary-postinc) (vl-unaryop-equiv x.op :vl-unary-postdec)) :otherwise nil)))
Theorem:
(defthm booleanp-of-vl-incexpr-post-p (b* ((post-p (vl-incexpr-post-p$inline x))) (booleanp post-p)) :rule-classes :type-prescription)
Theorem:
(defthm vl-incexpr-post-p$inline-of-vl-expr-fix-x (equal (vl-incexpr-post-p$inline (vl-expr-fix x)) (vl-incexpr-post-p$inline x)))
Theorem:
(defthm vl-incexpr-post-p$inline-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-incexpr-post-p$inline x) (vl-incexpr-post-p$inline x-equiv))) :rule-classes :congruence)