(vl-make-assertion-vardecls type vars loc) → vardecls
Function:
(defun vl-make-assertion-vardecls (type vars loc) (declare (xargs :guard (and (vl-datatype-p type) (vl-vardeclassignlist-p vars) (vl-location-p loc)))) (let ((__function__ 'vl-make-assertion-vardecls)) (declare (ignorable __function__)) (b* (((when (atom vars)) nil) ((vl-vardeclassign var1) (car vars))) (cons (make-vl-vardecl :name var1.id :type (vl-datatype-update-udims var1.dims type) :initval var1.rhs :loc loc) (vl-make-assertion-vardecls type (cdr vars) loc)))))
Theorem:
(defthm vl-vardecllist-p-of-vl-make-assertion-vardecls (b* ((vardecls (vl-make-assertion-vardecls type vars loc))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)