See vl-build-subsequent-portdecls. This is identical but for the vardecls instead of the portdecls.
(vl-build-subsequent-netdecls-for-ports x basedecl) → netdecls
Function:
(defun vl-build-subsequent-netdecls-for-ports (x basedecl) (declare (xargs :guard (and (vl-parsed-port-identifier-list-p x) (vl-vardecl-p basedecl)))) (let ((__function__ 'vl-build-subsequent-netdecls-for-ports)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) ((vl-parsed-port-identifier x1) (car x)) (basetype (vl-vardecl->type basedecl)) (- (or (not (vl-datatype->udims basetype)) (raise "Base datatype already has unpacked dimensions?"))) (type1 (if (consp x1.udims) (vl-datatype-update-udims x1.udims basetype) basetype))) (cons (change-vl-vardecl basedecl :name (vl-idtoken->name x1.name) :loc (vl-token->loc x1.name) :type type1) (vl-build-subsequent-netdecls-for-ports (cdr x) basedecl)))))
Theorem:
(defthm vl-vardecllist-p-of-vl-build-subsequent-netdecls-for-ports (b* ((netdecls (vl-build-subsequent-netdecls-for-ports x basedecl))) (vl-vardecllist-p netdecls)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-build-subsequent-netdecls-for-ports (b* ((netdecls (vl-build-subsequent-netdecls-for-ports x basedecl))) (true-listp netdecls)) :rule-classes :type-prescription)
Theorem:
(defthm len-of-vl-build-subsequent-netdecls (b* ((netdecls (vl-build-subsequent-netdecls-for-ports x basedecl))) (equal (len netdecls) (len x))) :rule-classes :rewrite)
Theorem:
(defthm consp-of-vl-build-subsequent-netdecls (b* ((netdecls (vl-build-subsequent-netdecls-for-ports x basedecl))) (equal (consp netdecls) (consp x))) :rule-classes :rewrite)
Theorem:
(defthm vl-build-subsequent-netdecls-under-iff (b* ((netdecls (vl-build-subsequent-netdecls-for-ports x basedecl))) (iff netdecls (consp x))) :rule-classes :rewrite)