Recursively check through an expression for precedence problems.
(vl-warn-odd-binary-expression x ss) → infos
Theorem:
(defthm return-type-of-vl-warn-odd-binary-expression.infos (b* ((?infos (vl-warn-odd-binary-expression x ss))) (vl-oddinfolist-p infos)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-vl-warn-odd-binary-expression-list.infos (b* ((?infos (vl-warn-odd-binary-expression-list x ss))) (vl-oddinfolist-p infos)) :rule-classes :rewrite)
Theorem:
(defthm vl-warn-odd-binary-expression-of-vl-expr-fix-x (equal (vl-warn-odd-binary-expression (vl-expr-fix x) ss) (vl-warn-odd-binary-expression x ss)))
Theorem:
(defthm vl-warn-odd-binary-expression-of-vl-scopestack-fix-ss (equal (vl-warn-odd-binary-expression x (vl-scopestack-fix ss)) (vl-warn-odd-binary-expression x ss)))
Theorem:
(defthm vl-warn-odd-binary-expression-list-of-vl-exprlist-fix-x (equal (vl-warn-odd-binary-expression-list (vl-exprlist-fix x) ss) (vl-warn-odd-binary-expression-list x ss)))
Theorem:
(defthm vl-warn-odd-binary-expression-list-of-vl-scopestack-fix-ss (equal (vl-warn-odd-binary-expression-list x (vl-scopestack-fix ss)) (vl-warn-odd-binary-expression-list x ss)))
Theorem:
(defthm vl-warn-odd-binary-expression-vl-expr-equiv-congruence-on-x (implies (vl-expr-equiv x x-equiv) (equal (vl-warn-odd-binary-expression x ss) (vl-warn-odd-binary-expression x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-odd-binary-expression-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-warn-odd-binary-expression x ss) (vl-warn-odd-binary-expression x ss-equiv))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-odd-binary-expression-list-vl-exprlist-equiv-congruence-on-x (implies (vl-exprlist-equiv x x-equiv) (equal (vl-warn-odd-binary-expression-list x ss) (vl-warn-odd-binary-expression-list x-equiv ss))) :rule-classes :congruence)
Theorem:
(defthm vl-warn-odd-binary-expression-list-vl-scopestack-equiv-congruence-on-ss (implies (vl-scopestack-equiv ss ss-equiv) (equal (vl-warn-odd-binary-expression-list x ss) (vl-warn-odd-binary-expression-list x ss-equiv))) :rule-classes :congruence)