(vl-modinsts-add-atts x atts) → xx
Function:
(defun vl-modinsts-add-atts (x atts) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-atts-p atts)))) (let ((__function__ 'vl-modinsts-add-atts)) (declare (ignorable __function__)) (if (atom x) nil (cons (change-vl-modinst (car x) :atts (append atts (vl-modinst->atts (car x)))) (vl-modinsts-add-atts (cdr x) atts)))))
Theorem:
(defthm vl-modinstlist-p-of-vl-modinsts-add-atts (implies (and (vl-modinstlist-p x) (vl-atts-p atts)) (b* ((xx (vl-modinsts-add-atts x atts))) (vl-modinstlist-p xx))) :rule-classes :rewrite)