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