		Search-engine friendly clone of the ACL2 documentation.

Vl-packeddimensionlist-allexprs

Vl-packeddimensionlist-allexprs-nrev

Signature
(vl-packeddimensionlist-allexprs-nrev x nrev) → nrev
Arguments: x — Guard (vl-packeddimensionlist-p x).

Definitions and Theorems

Function: vl-packeddimensionlist-allexprs-nrev

(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: vl-packeddimensionlist-allexprs-nrev-of-vl-packeddimensionlist-fix-x

(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: vl-packeddimensionlist-allexprs-nrev-vl-packeddimensionlist-equiv-congruence-on-x

(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)