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 (car x) cdr-portdecls) cdr-blockitems))) (mv cdr-portdecls (cons (car x) cdr-blockitems)))))
Theorem:
(defthm vl-portdecllist-p-of-vl-filter-portdecl-or-blockitem-list.portdecls (implies (and (force (vl-portdecl-or-blockitem-list-p x))) (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 (implies (and (force (vl-portdecl-or-blockitem-list-p x))) (b* (((mv ?portdecls ?blockitems) (vl-filter-portdecl-or-blockitem-list x))) (vl-blockitemlist-p blockitems))) :rule-classes :rewrite)