(vl-packagemap-find-packages-for-name name map) → names
Function:
(defun vl-packagemap-find-packages-for-name (name map) (declare (xargs :guard (and (stringp name) (vl-packagemap-p map)))) (let ((__function__ 'vl-packagemap-find-packages-for-name)) (declare (ignorable __function__)) (if (atom map) nil (if (and (mbt (consp (car map))) (hons-get (string-fix name) (vl-scopeitem-alist-fix (cdar map)))) (cons (string-fix (caar map)) (vl-packagemap-find-packages-for-name name (cdr map))) (vl-packagemap-find-packages-for-name name (cdr map))))))
Theorem:
(defthm string-listp-of-vl-packagemap-find-packages-for-name (b* ((names (vl-packagemap-find-packages-for-name name map))) (string-listp names)) :rule-classes :rewrite)
Theorem:
(defthm vl-packagemap-find-packages-for-name-of-str-fix-name (equal (vl-packagemap-find-packages-for-name (str-fix name) map) (vl-packagemap-find-packages-for-name name map)))
Theorem:
(defthm vl-packagemap-find-packages-for-name-streqv-congruence-on-name (implies (streqv name name-equiv) (equal (vl-packagemap-find-packages-for-name name map) (vl-packagemap-find-packages-for-name name-equiv map))) :rule-classes :congruence)
Theorem:
(defthm vl-packagemap-find-packages-for-name-of-vl-packagemap-fix-map (equal (vl-packagemap-find-packages-for-name name (vl-packagemap-fix map)) (vl-packagemap-find-packages-for-name name map)))
Theorem:
(defthm vl-packagemap-find-packages-for-name-vl-packagemap-equiv-congruence-on-map (implies (vl-packagemap-equiv map map-equiv) (equal (vl-packagemap-find-packages-for-name name map) (vl-packagemap-find-packages-for-name name map-equiv))) :rule-classes :congruence)