Split a list of cases into default and non-default cases.
(vl-filter-parsed-caseitemlist x) → (mv default-stmts normal-cases)
Function:
(defun vl-filter-parsed-caseitemlist (x) (declare (xargs :guard (vl-caselist-p x))) (let ((__function__ 'vl-filter-parsed-caseitemlist)) (declare (ignorable __function__)) (b* ((x (vl-caselist-fix x)) ((when (atom x)) (mv nil nil)) ((mv default-stmts normal-cases) (vl-filter-parsed-caseitemlist (cdr x))) ((cons exprs1 stmt1) (car x)) ((when exprs1) (mv default-stmts (cons (car x) normal-cases)))) (mv (cons stmt1 default-stmts) normal-cases))))
Theorem:
(defthm vl-stmtlist-p-of-vl-filter-parsed-caseitemlist.default-stmts (b* (((mv ?default-stmts ?normal-cases) (vl-filter-parsed-caseitemlist x))) (vl-stmtlist-p default-stmts)) :rule-classes :rewrite)
Theorem:
(defthm vl-caselist-p-of-vl-filter-parsed-caseitemlist.normal-cases (b* (((mv ?default-stmts ?normal-cases) (vl-filter-parsed-caseitemlist x))) (vl-caselist-p normal-cases)) :rule-classes :rewrite)
Theorem:
(defthm vl-filter-parsed-caseitemlist-mvtypes-0 (true-listp (mv-nth 0 (vl-filter-parsed-caseitemlist x))) :rule-classes :type-prescription)
Theorem:
(defthm vl-filter-parsed-caseitemlist-mvtypes-1 (true-listp (mv-nth 1 (vl-filter-parsed-caseitemlist x))) :rule-classes :type-prescription)