Make sure all match expressions have been sized and that their sizes are compatible with the test expression.
(vl-casestmt-sizes-agreep test cases) → *
Function:
(defun vl-casestmt-sizes-agreep (test cases) (declare (xargs :guard (and (vl-expr-p test) (vl-caselist-p cases)))) (let ((__function__ 'vl-casestmt-sizes-agreep)) (declare (ignorable __function__)) (b* ((cases (vl-caselist-fix cases)) ((when (atom cases)) t) ((cons match-exprs ?body1) (car cases))) (and (vl-casestmt-matchexpr-sizes-agreep test match-exprs) (vl-casestmt-sizes-agreep test (cdr cases))))))
Theorem:
(defthm vl-casestmt-sizes-agreep-when-atom (implies (atom cases) (equal (vl-casestmt-sizes-agreep test cases) t)))
Theorem:
(defthm vl-casestmt-sizes-agreep-of-cons (equal (vl-casestmt-sizes-agreep test (cons a cases)) (if (atom a) (vl-casestmt-sizes-agreep test cases) (and (vl-casestmt-matchexpr-sizes-agreep test (car a)) (vl-casestmt-sizes-agreep test cases)))))
Theorem:
(defthm vl-casestmt-sizes-agreep-of-vl-expr-fix-test (equal (vl-casestmt-sizes-agreep (vl-expr-fix test) cases) (vl-casestmt-sizes-agreep test cases)))
Theorem:
(defthm vl-casestmt-sizes-agreep-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-sizes-agreep test cases) (vl-casestmt-sizes-agreep test-equiv cases))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-sizes-agreep-of-vl-caselist-fix-cases (equal (vl-casestmt-sizes-agreep test (vl-caselist-fix cases)) (vl-casestmt-sizes-agreep test cases)))
Theorem:
(defthm vl-casestmt-sizes-agreep-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casestmt-sizes-agreep test cases) (vl-casestmt-sizes-agreep test cases-equiv))) :rule-classes :congruence)