		Search-engine friendly clone of the ACL2 documentation.

Oddexpr-check

Vl-warn-odd-binary-expression

Recursively check through an expression for precedence problems.

Signature
(vl-warn-odd-binary-expression x ss) → infos
Arguments: x — Subexpression we're recurring through.
Guard (vl-expr-p x).; ss — Guard (vl-scopestack-p ss).
Returns: infos — Type (vl-oddinfolist-p infos).

Theorem: return-type-of-vl-warn-odd-binary-expression.infos

(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: return-type-of-vl-warn-odd-binary-expression-list.infos

(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: vl-warn-odd-binary-expression-of-vl-expr-fix-x

(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: vl-warn-odd-binary-expression-of-vl-scopestack-fix-ss

(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: vl-warn-odd-binary-expression-list-of-vl-exprlist-fix-x

(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: vl-warn-odd-binary-expression-list-of-vl-scopestack-fix-ss

(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: vl-warn-odd-binary-expression-vl-expr-equiv-congruence-on-x

(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: vl-warn-odd-binary-expression-vl-scopestack-equiv-congruence-on-ss

(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: vl-warn-odd-binary-expression-list-vl-exprlist-equiv-congruence-on-x

(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: vl-warn-odd-binary-expression-list-vl-scopestack-equiv-congruence-on-ss

(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)

Subtopics

Vl-warn-odd-binary-expression-list