(vl-mark-wires-set x warnp alist) → new-alist
Function:
(defun vl-mark-wires-set (x warnp alist) (declare (xargs :guard (and (string-listp x) (vl-wireinfo-alistp alist)))) (let ((__function__ 'vl-mark-wires-set)) (declare (ignorable __function__)) (if (atom x) alist (let ((alist (vl-mark-wire-set (car x) warnp alist))) (vl-mark-wires-set (cdr x) warnp alist)))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-set (implies (and (force (string-listp x)) (force (vl-wireinfo-alistp alist))) (b* ((new-alist (vl-mark-wires-set x warnp alist))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)