(vl-mark-wires-for-assignlist x alist) → new-alist
Function:
(defun vl-mark-wires-for-assignlist (x alist) (declare (xargs :guard (and (vl-assignlist-p x) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-mark-wires-for-assignlist)) (declare (ignorable __function__)) (b* (((when (atom x)) alist) (alist (vl-mark-wires-for-assignment (car x) alist))) (vl-mark-wires-for-assignlist (cdr x) alist))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-assignlist (implies (and (force (vl-assignlist-p x)) (force (vl-wireinfo-alistp alist))) (b* ((new-alist (vl-mark-wires-for-assignlist x alist))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)