Collect expressions used in left-hand side positions.
(vl-stmt-cblock-lvalexprs x) → exprs
Theorem:
(defthm return-type-of-vl-stmt-cblock-lvalexprs.exprs (implies (and (force (vl-stmt-p x)) (force (vl-stmt-cblock-p x))) (b* ((?exprs (vl-stmt-cblock-lvalexprs x))) (and (vl-exprlist-p exprs) (vl-idexprlist-p exprs)))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-stmtlist-cblock-lvalexprs.exprs (implies (and (force (vl-stmtlist-p x)) (force (vl-stmtlist-cblock-p x))) (b* ((?exprs (vl-stmtlist-cblock-lvalexprs x))) (and (vl-exprlist-p exprs) (vl-idexprlist-p exprs)))) :rule-classes :rewrite)