(vl-foreach-vardecls-from-loopvars loc loopvars) → vardecls
Function:
(defun vl-foreach-vardecls-from-loopvars (loc loopvars) (declare (xargs :guard (and (vl-location-p loc) (vl-maybe-string-list-p loopvars)))) (let ((__function__ 'vl-foreach-vardecls-from-loopvars)) (declare (ignorable __function__)) (cond ((atom loopvars) nil) ((atom (car loopvars)) (vl-foreach-vardecls-from-loopvars loc (cdr loopvars))) (t (cons (make-vl-vardecl :name (car loopvars) :loc loc :type *vl-plain-old-integer-type*) (vl-foreach-vardecls-from-loopvars loc (cdr loopvars)))))))
Theorem:
(defthm vl-vardecllist-p-of-vl-foreach-vardecls-from-loopvars (b* ((vardecls (vl-foreach-vardecls-from-loopvars loc loopvars))) (vl-vardecllist-p vardecls)) :rule-classes :rewrite)