(vl-genelementlist->blocknames-nrev x nrev) → nrev
Function:
(defun vl-genelementlist->blocknames-nrev (x nrev) (declare (xargs :stobjs (nrev))) (declare (xargs :guard (vl-genelementlist-p x))) (let ((__function__ 'vl-genelementlist->blocknames-nrev)) (declare (ignorable __function__)) (b* (((when (atom x)) (nrev-fix nrev)) (name (vl-genelement->blockname (car x))) (nrev (if name (nrev-push name nrev) nrev))) (vl-genelementlist->blocknames-nrev (cdr x) nrev))))
Theorem:
(defthm vl-genelementlist->blocknames-nrev-of-vl-genelementlist-fix-x (equal (vl-genelementlist->blocknames-nrev (vl-genelementlist-fix x) nrev) (vl-genelementlist->blocknames-nrev x nrev)))
Theorem:
(defthm vl-genelementlist->blocknames-nrev-vl-genelementlist-equiv-congruence-on-x (implies (vl-genelementlist-equiv x x-equiv) (equal (vl-genelementlist->blocknames-nrev x nrev) (vl-genelementlist->blocknames-nrev x-equiv nrev))) :rule-classes :congruence)