(vl-make-structmembers atts rand type decls) → decls
Function:
(defun vl-make-structmembers (atts rand type decls) (declare (xargs :guard (and (vl-atts-p atts) (vl-randomqualifier-p rand) (vl-datatype-p type) (vl-vardeclassignlist-p decls)))) (let ((__function__ 'vl-make-structmembers)) (declare (ignorable __function__)) (b* (((when (atom decls)) nil) ((vl-vardeclassign decl) (car decls))) (cons (make-vl-structmember :atts atts :rand rand :type (vl-datatype-update-udims decl.dims type) :name decl.id :rhs decl.expr) (vl-make-structmembers atts rand type (cdr decls))))))
Theorem:
(defthm vl-structmemberlist-p-of-vl-make-structmembers (implies (and (force (vl-atts-p atts)) (force (vl-randomqualifier-p rand)) (force (vl-datatype-p type)) (force (vl-vardeclassignlist-p decls))) (b* ((decls (vl-make-structmembers atts rand type decls))) (vl-structmemberlist-p decls))) :rule-classes :rewrite)