Collect all conditions from if statements in an edgesynth statement.
(vl-edgesynth-stmt-conditions x) → rhses
Theorem:
(defthm return-type-of-vl-edgesynth-stmt-conditions.rhses (implies (and (force (vl-stmt-p x)) (force (vl-edgesynth-stmt-p x))) (b* ((?rhses (vl-edgesynth-stmt-conditions x))) (vl-exprlist-p rhses))) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-edgesynth-stmtlist-conditions.conditions (implies (and (force (vl-stmtlist-p x)) (force (vl-edgesynth-stmtlist-p x))) (b* ((?conditions (vl-edgesynth-stmtlist-conditions x))) (vl-exprlist-p conditions))) :rule-classes :rewrite)