(vl-delete-duplicated-genelement-blocknames alist) → filtered-alist
Function:
(defun vl-delete-duplicated-genelement-blocknames (alist) (declare (xargs :guard (vl-scopeitem-alist-p alist))) (let ((__function__ 'vl-delete-duplicated-genelement-blocknames)) (declare (ignorable __function__)) (b* ((alist (vl-scopeitem-alist-fix alist)) (names (alist-keys alist)) (dupes (duplicated-members names))) (vl-remove-keys dupes alist))))
Theorem:
(defthm vl-scopeitem-alist-p-of-vl-delete-duplicated-genelement-blocknames (b* ((filtered-alist (vl-delete-duplicated-genelement-blocknames alist))) (vl-scopeitem-alist-p filtered-alist)) :rule-classes :rewrite)
Theorem:
(defthm vl-delete-duplicated-genelement-blocknames-of-vl-scopeitem-alist-fix-alist (equal (vl-delete-duplicated-genelement-blocknames (vl-scopeitem-alist-fix alist)) (vl-delete-duplicated-genelement-blocknames alist)))
Theorem:
(defthm vl-delete-duplicated-genelement-blocknames-vl-scopeitem-alist-equiv-congruence-on-alist (implies (vl-scopeitem-alist-equiv alist alist-equiv) (equal (vl-delete-duplicated-genelement-blocknames alist) (vl-delete-duplicated-genelement-blocknames alist-equiv))) :rule-classes :congruence)