(vl-casestmt-size-warnings-aux test cases ctx) → warnings
Function:
(defun vl-casestmt-size-warnings-aux (test cases ctx) (declare (xargs :guard (and (vl-expr-p test) (vl-caselist-p cases) (vl-modelement-p ctx)))) (let ((__function__ 'vl-casestmt-size-warnings-aux)) (declare (ignorable __function__)) (b* ((test (vl-expr-fix test)) (cases (vl-caselist-fix cases)) (ctx (vl-modelement-fix ctx)) ((when (atom cases)) nil) ((cons match-exprs1 ?body1) (car cases)) (first (vl-casestmt-matchexpr-size-warnings test match-exprs1 ctx)) (rest (vl-casestmt-size-warnings-aux test (cdr cases) ctx))) (append first rest))))
Theorem:
(defthm vl-warninglist-p-of-vl-casestmt-size-warnings-aux (b* ((warnings (vl-casestmt-size-warnings-aux test cases ctx))) (vl-warninglist-p warnings)) :rule-classes :rewrite)
Theorem:
(defthm true-listp-of-vl-casestmt-size-warnings-aux (b* ((warnings (vl-casestmt-size-warnings-aux test cases ctx))) (true-listp warnings)) :rule-classes :type-prescription)
Theorem:
(defthm vl-casestmt-size-warnings-aux-correct (implies (not (vl-casestmt-size-warnings-aux test cases ctx)) (vl-casestmt-sizes-agreep test cases)))
Theorem:
(defthm vl-casestmt-size-warnings-aux-of-vl-expr-fix-test (equal (vl-casestmt-size-warnings-aux (vl-expr-fix test) cases ctx) (vl-casestmt-size-warnings-aux test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-aux-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-size-warnings-aux test cases ctx) (vl-casestmt-size-warnings-aux test-equiv cases ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-size-warnings-aux-of-vl-caselist-fix-cases (equal (vl-casestmt-size-warnings-aux test (vl-caselist-fix cases) ctx) (vl-casestmt-size-warnings-aux test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-aux-vl-caselist-equiv-congruence-on-cases (implies (vl-caselist-equiv cases cases-equiv) (equal (vl-casestmt-size-warnings-aux test cases ctx) (vl-casestmt-size-warnings-aux test cases-equiv ctx))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-size-warnings-aux-of-vl-modelement-fix-ctx (equal (vl-casestmt-size-warnings-aux test cases (vl-modelement-fix ctx)) (vl-casestmt-size-warnings-aux test cases ctx)))
Theorem:
(defthm vl-casestmt-size-warnings-aux-vl-modelement-equiv-congruence-on-ctx (implies (vl-modelement-equiv ctx ctx-equiv) (equal (vl-casestmt-size-warnings-aux test cases ctx) (vl-casestmt-size-warnings-aux test cases ctx-equiv))) :rule-classes :congruence)