		Search-engine friendly clone of the ACL2 documentation.

Nameclash

Vl-nameclash-collect-local-decls

Signature
(vl-nameclash-collect-local-decls name alist) → items
Arguments: name — Guard (stringp name).; alist — Guard (vl-scopeitem-alist-p alist).
Returns: items — Type (vl-scopeitemlist-p items).

Definitions and Theorems

Function: vl-nameclash-collect-local-decls

(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: vl-scopeitemlist-p-of-vl-nameclash-collect-local-decls

(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)