(vl-make-tf-ports-from-parsed-ids ids &key dir type atts) → ports
Function:
(defun vl-make-tf-ports-from-parsed-ids-fn (ids dir type atts) (declare (xargs :guard (and (vl-tf-parsed-var-idlist-p ids) (vl-direction-p dir) (vl-datatype-p type) (vl-atts-p atts)))) (let ((__function__ 'vl-make-tf-ports-from-parsed-ids)) (declare (ignorable __function__)) (b* (((when (atom ids)) nil) ((vl-tf-parsed-var-id id1) (car ids))) (cons (make-vl-portdecl :name (vl-idtoken->name id1.name) :loc (vl-token->loc id1.name) :nettype nil :dir dir :type (vl-datatype-update-udims id1.udims type) :default id1.default :atts atts) (vl-make-tf-ports-from-parsed-ids (cdr ids) :dir dir :type type :atts atts)))))
Theorem:
(defthm vl-portdecllist-p-of-vl-make-tf-ports-from-parsed-ids (b* ((ports (vl-make-tf-ports-from-parsed-ids-fn ids dir type atts))) (vl-portdecllist-p ports)) :rule-classes :rewrite)