		Search-engine friendly clone of the ACL2 documentation.

Argresolve

Vl-make-namedarg-alist

Build a fast alist associating the name of each port declaration with the whole vl-namedarg-p object.

Signature
(vl-make-namedarg-alist x) → palist
Arguments: x — Guard (vl-namedarglist-p x).
Returns: palist — Type (vl-namedarg-alist-p palist), given the guard.

Definitions and Theorems

Function: vl-make-namedarg-alist

(defun vl-make-namedarg-alist (x)
  (declare (xargs :guard (vl-namedarglist-p x)))
  (let ((__function__ 'vl-make-namedarg-alist))
    (declare (ignorable __function__))
    (make-fast-alist (vl-namedarglist-alist x nil))))

Theorem: vl-namedarg-alist-p-of-vl-make-namedarg-alist

(defthm vl-namedarg-alist-p-of-vl-make-namedarg-alist
  (implies (and (vl-namedarglist-p x))
           (b* ((palist (vl-make-namedarg-alist x)))
             (vl-namedarg-alist-p palist)))
  :rule-classes :rewrite)

Theorem: alistp-of-vl-make-namedarg-alist

(defthm alistp-of-vl-make-namedarg-alist
  (alistp (vl-make-namedarg-alist x)))

Theorem: hons-assoc-equal-of-vl-make-namedarg-alist

(defthm hons-assoc-equal-of-vl-make-namedarg-alist
  (implies (stringp k)
           (equal (hons-assoc-equal k (vl-make-namedarg-alist x))
                  (and (vl-find-namedarg k x)
                       (cons k (vl-find-namedarg k x))))))

Theorem: vl-make-namedarg-alist-of-vl-namedarglist-fix-x

(defthm vl-make-namedarg-alist-of-vl-namedarglist-fix-x
  (equal (vl-make-namedarg-alist (vl-namedarglist-fix x))
         (vl-make-namedarg-alist x)))

Theorem: vl-make-namedarg-alist-vl-namedarglist-equiv-congruence-on-x

(defthm vl-make-namedarg-alist-vl-namedarglist-equiv-congruence-on-x
  (implies (vl-namedarglist-equiv x x-equiv)
           (equal (vl-make-namedarg-alist x)
                  (vl-make-namedarg-alist x-equiv)))
  :rule-classes :congruence)