Collect all instance names declared in a vl-gateinstlist-p.
(vl-gateinstlist->names x) → names
Note that gate instances may be unnamed, in which case we do not add anything. In other words, the list of names returned may be shorter than the number of gate instances in the list.
Function:
(defun vl-gateinstlist->names (x) (declare (xargs :guard (vl-gateinstlist-p x))) (let ((__function__ 'vl-gateinstlist->names)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (if (vl-gateinst->name (car x)) (cons (vl-gateinst->name (car x)) (vl-gateinstlist->names (cdr x))) (vl-gateinstlist->names (cdr x))) nil) :exec (with-local-nrev (vl-gateinstlist->names-nrev x nrev)))))
Theorem:
(defthm string-listp-of-vl-gateinstlist->names (b* ((names (vl-gateinstlist->names x))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm vl-gateinstlist->names-nrev-removal (equal (vl-gateinstlist->names-nrev x nrev) (append nrev (vl-gateinstlist->names x))))
Theorem:
(defthm vl-gateinstlist->names-when-not-consp (implies (not (consp x)) (equal (vl-gateinstlist->names x) nil)))
Theorem:
(defthm vl-gateinstlist->names-of-cons (equal (vl-gateinstlist->names (cons a x)) (if (vl-gateinst->name a) (cons (vl-gateinst->name a) (vl-gateinstlist->names x)) (vl-gateinstlist->names x))))
Theorem:
(defthm vl-gateinstlist->names-of-list-fix (equal (vl-gateinstlist->names (list-fix x)) (vl-gateinstlist->names x)))
Theorem:
(defthm vl-gateinstlist->names-preserves-list-equiv (implies (list-equiv x x-equiv) (equal (vl-gateinstlist->names x) (vl-gateinstlist->names x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-gateinstlist->names-of-append (equal (vl-gateinstlist->names (append x y)) (append (vl-gateinstlist->names x) (vl-gateinstlist->names y))))
Theorem:
(defthm vl-gateinstlist->names-of-rev (equal (vl-gateinstlist->names (rev x)) (rev (vl-gateinstlist->names x))))
Theorem:
(defthm vl-gateinstlist->names-of-vl-gateinstlist-fix-x (equal (vl-gateinstlist->names (vl-gateinstlist-fix x)) (vl-gateinstlist->names x)))
Theorem:
(defthm vl-gateinstlist->names-vl-gateinstlist-equiv-congruence-on-x (implies (vl-gateinstlist-equiv x x-equiv) (equal (vl-gateinstlist->names x) (vl-gateinstlist->names x-equiv))) :rule-classes :congruence)