(vl-port/vardecllist->portdecls x) → portdecls
Function:
(defun vl-port/vardecllist->portdecls (x) (declare (xargs :guard (vl-port/vardecllist-p x))) (let ((__function__ 'vl-port/vardecllist->portdecls)) (declare (ignorable __function__)) (cond ((atom x) nil) ((mbe :logic (vl-portdecl-p (car x)) :exec (eq (tag (car x)) :vl-portdecl)) (cons (car x) (vl-port/vardecllist->portdecls (cdr x)))) (t (vl-port/vardecllist->portdecls (cdr x))))))
Theorem:
(defthm vl-portdecllist-p-of-vl-port/vardecllist->portdecls (b* ((portdecls (vl-port/vardecllist->portdecls x))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)