Split out port declarations from other block items.
(vl-filter-portdecl-or-blockitem-list x) → (mv portdecls blockitems)
Function:
(defun vl-filter-portdecl-or-blockitem-list (x) (declare (xargs :guard (vl-portdecl-or-blockitem-list-p x))) (let ((__function__ 'vl-filter-portdecl-or-blockitem-list)) (declare (ignorable __function__)) (b* (((when (atom x)) (mv nil nil)) ((mv cdr-portdecls cdr-blockitems) (vl-filter-portdecl-or-blockitem-list (cdr x))) ((when (eq (tag (car x)) :vl-portdecl)) (mv (cons (vl-portdecl-fix (car x)) cdr-portdecls) cdr-blockitems))) (mv cdr-portdecls (cons (vl-blockitem-fix (car x)) cdr-blockitems)))))
Theorem:
(defthm vl-portdecllist-p-of-vl-filter-portdecl-or-blockitem-list.portdecls (b* (((mv ?portdecls ?blockitems) (vl-filter-portdecl-or-blockitem-list x))) (vl-portdecllist-p portdecls)) :rule-classes :rewrite)
Theorem:
(defthm vl-blockitemlist-p-of-vl-filter-portdecl-or-blockitem-list.blockitems (b* (((mv ?portdecls ?blockitems) (vl-filter-portdecl-or-blockitem-list x))) (vl-blockitemlist-p blockitems)) :rule-classes :rewrite)