Look throughout an expression for any
(vl-expr-arith-compare-check x ss) → warnings
We look through the expression
Theorem:
(defthm return-type-of-vl-expr-arith-compare-check.warnings (b* ((?warnings (vl-expr-arith-compare-check x ss))) (and (vl-warninglist-p warnings) (true-listp warnings))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-exprlist-arith-compare-check.warnings (b* ((?warnings (vl-exprlist-arith-compare-check x ss))) (vl-warninglist-p warnings)) :rule-classes :rewrite)