(vl-cblock-make-assigns names vars body ctx) → assigns
Function:
(defun vl-cblock-make-assigns (names vars body ctx) (declare (xargs :guard (and (string-listp names) (vl-vardecllist-p vars) (vl-stmt-p body) (vl-always-p ctx)))) (declare (xargs :guard (vl-stmt-cblock-p body))) (let ((__function__ 'vl-cblock-make-assigns)) (declare (ignorable __function__)) (if (atom names) nil (append (vl-cblock-make-assign (car names) vars body ctx) (vl-cblock-make-assigns (cdr names) vars body ctx)))))
Theorem:
(defthm vl-assignlist-p-of-vl-cblock-make-assigns (implies (and (force (string-listp names)) (force (vl-vardecllist-p vars)) (force (vl-stmt-p body)) (force (vl-always-p ctx)) (force (vl-stmt-cblock-p body))) (b* ((assigns (vl-cblock-make-assigns names vars body ctx))) (vl-assignlist-p assigns))) :rule-classes :rewrite)