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