Drop any blank ports from a list of ports.
(vl-portlist-drop-blankports x) → new-x
Function:
(defun vl-portlist-drop-blankports (x) (declare (xargs :guard (vl-portlist-p x))) (let ((__function__ 'vl-portlist-drop-blankports)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (x1 (vl-port-fix (car x))) ((when (or (eq (tag x1) :vl-interfaceport) (vl-regularport->expr (car x)))) (cons (vl-port-fix (car x)) (vl-portlist-drop-blankports (cdr x))))) (vl-portlist-drop-blankports (cdr x)))))
Theorem:
(defthm vl-portlist-p-of-vl-portlist-drop-blankports (b* ((new-x (vl-portlist-drop-blankports x))) (vl-portlist-p new-x)) :rule-classes :rewrite)