Function:
(defun vl-inc-or-dec-expr (var op) (declare (xargs :guard (and (vl-expr-p var) (member op '(:vl-plusplus :vl-minusminus))))) (let ((__function__ 'vl-inc-or-dec-expr)) (declare (ignorable __function__)) (make-vl-binary :op (if (eq op :vl-plusplus) :vl-binary-plus :vl-binary-minus) :left var :right (make-vl-literal :val (make-vl-constint :origwidth 32 :value 1 :origsign :vl-unsigned :wasunsized t)))))
Theorem:
(defthm vl-expr-p-of-vl-inc-or-dec-expr (b* ((expr (vl-inc-or-dec-expr var op))) (vl-expr-p expr)) :rule-classes :rewrite)