(vl-assign-lvalexprs-nrev x nrev) → nrev
Function:
(defun vl-assign-lvalexprs-nrev$inline (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-assign-p x))) (let ((__function__ 'vl-assign-lvalexprs-nrev)) (declare (ignorable __function__)) (b* ((x (vl-assign-fix x))) (b* (((vl-assign x) x)) (if (vl-expr-lvaluep x.lvalue) (nrev-push x.lvalue nrev) (prog2$ (cw "vl-assign-lvalexprs: skipping ill-formed lvalue~%") (nrev-fix nrev)))))))
Theorem:
(defthm vl-assign-lvalexprs-nrev$inline-of-vl-assign-fix-x (equal (vl-assign-lvalexprs-nrev$inline (vl-assign-fix x) nrev) (vl-assign-lvalexprs-nrev$inline x nrev)))
Theorem:
(defthm vl-assign-lvalexprs-nrev$inline-vl-assign-equiv-congruence-on-x (implies (vl-assign-equiv x x-equiv) (equal (vl-assign-lvalexprs-nrev$inline x nrev) (vl-assign-lvalexprs-nrev$inline x-equiv nrev))) :rule-classes :congruence)