(vl-casestmt-matchexpr-sizes-agreep test match-exprs) → *
Function:
(defun vl-casestmt-matchexpr-sizes-agreep (test match-exprs) (declare (xargs :guard (and (vl-expr-p test) (vl-exprlist-p match-exprs)))) (let ((__function__ 'vl-casestmt-matchexpr-sizes-agreep)) (declare (ignorable __function__)) (b* (((when (atom match-exprs)) t) (expr1 (car match-exprs))) (and (vl-expr->finaltype expr1) (eql (vl-expr->finalwidth test) (vl-expr->finalwidth expr1)) (vl-casestmt-matchexpr-sizes-agreep test (cdr match-exprs))))))
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-when-atom (implies (atom match-exprs) (vl-casestmt-matchexpr-sizes-agreep test match-exprs)))
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-of-cons (equal (vl-casestmt-matchexpr-sizes-agreep test (cons expr1 match-exprs)) (and (vl-expr->finaltype expr1) (equal (vl-expr->finalwidth test) (vl-expr->finalwidth expr1)) (vl-casestmt-matchexpr-sizes-agreep test match-exprs))))
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-of-vl-expr-fix-test (equal (vl-casestmt-matchexpr-sizes-agreep (vl-expr-fix test) match-exprs) (vl-casestmt-matchexpr-sizes-agreep test match-exprs)))
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-vl-expr-equiv-congruence-on-test (implies (vl-expr-equiv test test-equiv) (equal (vl-casestmt-matchexpr-sizes-agreep test match-exprs) (vl-casestmt-matchexpr-sizes-agreep test-equiv match-exprs))) :rule-classes :congruence)
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-of-vl-exprlist-fix-match-exprs (equal (vl-casestmt-matchexpr-sizes-agreep test (vl-exprlist-fix match-exprs)) (vl-casestmt-matchexpr-sizes-agreep test match-exprs)))
Theorem:
(defthm vl-casestmt-matchexpr-sizes-agreep-vl-exprlist-equiv-congruence-on-match-exprs (implies (vl-exprlist-equiv match-exprs match-exprs-equiv) (equal (vl-casestmt-matchexpr-sizes-agreep test match-exprs) (vl-casestmt-matchexpr-sizes-agreep test match-exprs-equiv))) :rule-classes :congruence)