(vl-packeddimensionlist-allexprs-nrev x nrev) → nrev
Function:
(defun vl-packeddimensionlist-allexprs-nrev (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-packeddimensionlist-p x))) (let ((__function__ 'vl-packeddimensionlist-allexprs-nrev)) (declare (ignorable __function__)) (if (atom x) (nrev-fix nrev) (let ((nrev (vl-packeddimension-allexprs-nrev (car x) nrev))) (vl-packeddimensionlist-allexprs-nrev (cdr x) nrev)))))
Theorem:
(defthm vl-packeddimensionlist-allexprs-nrev-of-vl-packeddimensionlist-fix-x (equal (vl-packeddimensionlist-allexprs-nrev (vl-packeddimensionlist-fix x) nrev) (vl-packeddimensionlist-allexprs-nrev x nrev)))
Theorem:
(defthm vl-packeddimensionlist-allexprs-nrev-vl-packeddimensionlist-equiv-congruence-on-x (implies (vl-packeddimensionlist-equiv x x-equiv) (equal (vl-packeddimensionlist-allexprs-nrev x nrev) (vl-packeddimensionlist-allexprs-nrev x-equiv nrev))) :rule-classes :congruence)