Drop arguments to blank ports from an plain argument list.
(vl-plainarglist-drop-blankports args ports) → new-args
Function:
(defun vl-plainarglist-drop-blankports (args ports) (declare (xargs :guard (and (vl-plainarglist-p args) (vl-portlist-p ports)))) (declare (xargs :guard (same-lengthp args ports))) (let ((__function__ 'vl-plainarglist-drop-blankports)) (declare (ignorable __function__)) (b* (((when (atom args)) nil) (port1 (vl-port-fix (car ports))) ((when (or (eq (tag port1) :vl-interfaceport) (vl-regularport->expr port1))) (cons (vl-plainarg-fix (car args)) (vl-plainarglist-drop-blankports (cdr args) (cdr ports))))) (vl-plainarglist-drop-blankports (cdr args) (cdr ports)))))
Theorem:
(defthm vl-plainarglist-p-of-vl-plainarglist-drop-blankports (b* ((new-args (vl-plainarglist-drop-blankports args ports))) (vl-plainarglist-p new-args)) :rule-classes :rewrite)