(vl-modinstlist-remove-interfaces x ss) → filtered-x
Function:
(defun vl-modinstlist-remove-interfaces (x ss) (declare (xargs :guard (and (vl-modinstlist-p x) (vl-scopestack-p ss)))) (let ((__function__ 'vl-modinstlist-remove-interfaces)) (declare (ignorable __function__)) (b* (((when (atom x)) nil) (dfn (vl-scopestack-find-definition (vl-modinst->modname (car x)) ss)) ((when (mbe :logic (vl-interface-p dfn) :exec (eq (tag dfn) :vl-interface))) (vl-modinstlist-remove-interfaces (cdr x) ss))) (cons (vl-modinst-fix (car x)) (vl-modinstlist-remove-interfaces (cdr x) ss)))))
Theorem:
(defthm vl-modinstlist-p-of-vl-modinstlist-remove-interfaces (b* ((filtered-x (vl-modinstlist-remove-interfaces x ss))) (vl-modinstlist-p filtered-x)) :rule-classes :rewrite)