Create an initial wireinfo alist by we associating each wire with a new vl-wireinfo entry.
(vl-make-initial-wireinfo-alist x) → alist
Function:
(defun vl-make-initial-wireinfo-alist (x) (declare (xargs :guard (string-listp x))) (let ((__function__ 'vl-make-initial-wireinfo-alist)) (declare (ignorable __function__)) (if (atom x) nil (hons-acons (car x) (make-vl-wireinfo :usedp nil :setp nil) (vl-make-initial-wireinfo-alist (cdr x))))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-make-initial-wireinfo-alist (implies (and (force (string-listp x))) (b* ((alist (vl-make-initial-wireinfo-alist x))) (vl-wireinfo-alistp alist))) :rule-classes :rewrite)