(vl-genelementlist->portdecls x) → portdecls
Function:
(defun vl-genelementlist->portdecls (x) (declare (xargs :guard (vl-genelementlist-p x))) (let ((__function__ 'vl-genelementlist->portdecls)) (declare (ignorable __function__)) (if (atom x) nil (if (and (eq (vl-genelement-kind (car x)) :vl-genbase) (eq (tag (vl-genbase->item (car x))) :vl-portdecl)) (cons (vl-genbase->item (car x)) (vl-genelementlist->portdecls (cdr x))) (vl-genelementlist->portdecls (cdr x))))))
Theorem:
(defthm vl-portdecllist-p-of-vl-genelementlist->portdecls (b* ((portdecls (vl-genelementlist->portdecls x))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)