(vl-nameclash-collect-local-decls name alist) → items
Function:
(defun vl-nameclash-collect-local-decls (name alist) (declare (xargs :guard (and (stringp name) (vl-scopeitem-alist-p alist)))) (let ((__function__ 'vl-nameclash-collect-local-decls)) (declare (ignorable __function__)) (b* (((when (atom alist)) nil) ((cons key val) (car alist)) ((when (streqv key name)) (cons (vl-scopeitem-fix val) (vl-nameclash-collect-local-decls name (cdr alist))))) (vl-nameclash-collect-local-decls name (cdr alist)))))
Theorem:
(defthm vl-scopeitemlist-p-of-vl-nameclash-collect-local-decls (b* ((items (vl-nameclash-collect-local-decls name alist))) (vl-scopeitemlist-p items)) :rule-classes :rewrite)