Collect all names introduced by a vl-descriptionlist-p.
(vl-descriptionlist->names x) → *
Note that descriptions may not have names, in which case we don't add anything. In other words, the list of names returned may be shorter than the number of descriptions in the list.
Function:
(defun vl-descriptionlist->names (x) (declare (xargs :guard (vl-descriptionlist-p x))) (let ((__function__ 'vl-descriptionlist->names)) (declare (ignorable __function__)) (mbe :logic (if (consp x) (if (vl-description->name (car x)) (cons (vl-description->name (car x)) (vl-descriptionlist->names (cdr x))) (vl-descriptionlist->names (cdr x))) nil) :exec (with-local-nrev (vl-descriptionlist->names-nrev x nrev)))))
Theorem:
(defthm vl-descriptionlist->names-nrev-removal (equal (vl-descriptionlist->names-nrev x nrev) (append nrev (vl-descriptionlist->names x))))
Theorem:
(defthm vl-descriptionlist->names-when-not-consp (implies (not (consp x)) (equal (vl-descriptionlist->names x) nil)))
Theorem:
(defthm vl-descriptionlist->names-of-cons (equal (vl-descriptionlist->names (cons a x)) (if (vl-description->name a) (cons (vl-description->name a) (vl-descriptionlist->names x)) (vl-descriptionlist->names x))))
Theorem:
(defthm vl-descriptionlist->names-of-list-fix (equal (vl-descriptionlist->names (list-fix x)) (vl-descriptionlist->names x)))
Theorem:
(defthm vl-descriptionlist->names-preserves-list-equiv (implies (list-equiv x x-equiv) (equal (vl-descriptionlist->names x) (vl-descriptionlist->names x-equiv))) :rule-classes (:congruence))
Theorem:
(defthm vl-descriptionlist->names-of-append (equal (vl-descriptionlist->names (append x y)) (append (vl-descriptionlist->names x) (vl-descriptionlist->names y))))
Theorem:
(defthm vl-descriptionlist->names-of-rev (equal (vl-descriptionlist->names (rev x)) (rev (vl-descriptionlist->names x))))
Theorem:
(defthm string-listp-of-vl-descriptionlist->names (string-listp (vl-descriptionlist->names x)))
Theorem:
(defthm no-nil-in-vl-descriptionlist->names (not (member nil (vl-descriptionlist->names x))))
Theorem:
(defthm vl-descriptionlist->names-of-vl-descriptionlist-fix-x (equal (vl-descriptionlist->names (vl-descriptionlist-fix x)) (vl-descriptionlist->names x)))
Theorem:
(defthm vl-descriptionlist->names-vl-descriptionlist-equiv-congruence-on-x (implies (vl-descriptionlist-equiv x x-equiv) (equal (vl-descriptionlist->names x) (vl-descriptionlist->names x-equiv))) :rule-classes :congruence)