(vl-make-udp-portdecls ids dir type atts) → portdecls
Function:
(defun vl-make-udp-portdecls (ids dir type atts) (declare (xargs :guard (and (vl-idtoken-list-p ids) (vl-direction-p dir) (vl-datatype-p type) (vl-atts-p atts)))) (let ((__function__ 'vl-make-udp-portdecls)) (declare (ignorable __function__)) (if (atom ids) nil (cons (make-vl-portdecl :loc (vl-token->loc (car ids)) :name (vl-idtoken->name (car ids)) :dir dir :type type :atts atts) (vl-make-udp-portdecls (cdr ids) dir type atts)))))
Theorem:
(defthm vl-portdecllist-p-of-vl-make-udp-portdecls (b* ((portdecls (vl-make-udp-portdecls ids dir type atts))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)
Theorem:
(defthm len-of-vl-make-udp-portdecls (b* ((portdecls (vl-make-udp-portdecls ids dir type atts))) (equal (len portdecls) (len ids))) :rule-classes :rewrite)