(vl-build-netdecls-aux x basedecl baseassign) → (mv nets assigns)
Function:
(defun vl-build-netdecls-aux (x basedecl baseassign) (declare (xargs :guard (and (vl-vardeclassignlist-p x) (vl-vardecl-p basedecl) (vl-assign-p baseassign)))) (declare (xargs :guard (vl-vardeclassignlist-newfree-p x))) (let ((__function__ 'vl-build-netdecls-aux)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((vl-vardeclassign x1) (car x)) (type (vl-vardecl->type basedecl)) (type (if (consp x1.dims) (vl-datatype-update-udims x1.dims type) type)) (vardecl (change-vl-vardecl basedecl :name x1.id :type type :delay (and (not x1.rhs) (vl-assign->delay baseassign)))) (assign (and x1.rhs (change-vl-assign baseassign :lvalue (vl-idexpr x1.id) :expr (vl-rhsexpr->guts x1.rhs)))) ((mv rest-decls rest-assigns) (vl-build-netdecls-aux (cdr x) basedecl baseassign))) (mv (cons vardecl rest-decls) (if assign (cons assign rest-assigns) rest-assigns)))))
Theorem:
(defthm vl-vardecllist-p-of-vl-build-netdecls-aux.nets (b* (((mv ?nets ?assigns) (vl-build-netdecls-aux x basedecl baseassign))) (vl-vardecllist-p nets)) :rule-classes :rewrite)
Theorem:
(defthm vl-assignlist-p-of-vl-build-netdecls-aux.assigns (b* (((mv ?nets ?assigns) (vl-build-netdecls-aux x basedecl baseassign))) (vl-assignlist-p assigns)) :rule-classes :rewrite)
Theorem:
(defthm vl-build-netdecls-aux-mvtypes-0 (true-listp (mv-nth 0 (vl-build-netdecls-aux x basedecl baseassign))) :rule-classes :type-prescription)
Theorem:
(defthm vl-build-netdecls-aux-mvtypes-1 (true-listp (mv-nth 1 (vl-build-netdecls-aux x basedecl baseassign))) :rule-classes :type-prescription)