(vl-mark-wires-for-plainarglist x alist warning-wires) → (mv new-alist warning-wires)
Function:
(defun vl-mark-wires-for-plainarglist (x alist warning-wires) (declare (xargs :guard (and (vl-plainarglist-p x) (vl-wireinfo-alistp alist) (string-listp warning-wires)))) (let ((__function__ 'vl-mark-wires-for-plainarglist)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv alist warning-wires)) ((mv alist warning-wires) (vl-mark-wires-for-plainarg (car x) alist warning-wires))) (vl-mark-wires-for-plainarglist (cdr x) alist warning-wires))))
Theorem:
(defthm vl-wireinfo-alistp-of-vl-mark-wires-for-plainarglist.new-alist (implies (and (force (vl-plainarglist-p x)) (force (vl-wireinfo-alistp alist)) (force (string-listp warning-wires))) (b* (((mv ?new-alist ?warning-wires) (vl-mark-wires-for-plainarglist x alist warning-wires))) (vl-wireinfo-alistp new-alist))) :rule-classes :rewrite)
Theorem:
(defthm string-listp-of-vl-mark-wires-for-plainarglist.warning-wires (implies (and (force (vl-plainarglist-p x)) (force (vl-wireinfo-alistp alist)) (force (string-listp warning-wires))) (b* (((mv ?new-alist ?warning-wires) (vl-mark-wires-for-plainarglist x alist warning-wires))) (string-listp warning-wires))) :rule-classes :rewrite)