		Search-engine friendly clone of the ACL2 documentation.

Increment-elim

Vl-expr-incexprs

Gather all increment/decrement/assignment expressions from an expression.

Signature
(vl-expr-incexprs x) → incexprs
Arguments: x — Guard (vl-expr-p x).
Returns: incexprs — Type (and (vl-exprlist-p incexprs) (vl-incexprlist-p incexprs)).

Theorem: return-type-of-vl-expr-incexprs.incexprs

(defthm return-type-of-vl-expr-incexprs.incexprs
  (b* ((?incexprs (vl-expr-incexprs x)))
    (and (vl-exprlist-p incexprs)
         (vl-incexprlist-p incexprs)))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-incexprs.incexprs

(defthm return-type-of-vl-exprlist-incexprs.incexprs
  (b* ((?incexprs (vl-exprlist-incexprs x)))
    (and (vl-exprlist-p incexprs)
         (vl-incexprlist-p incexprs)))
  :rule-classes :rewrite)

Theorem: vl-expr-incexprs-of-vl-expr-fix-x

(defthm vl-expr-incexprs-of-vl-expr-fix-x
  (equal (vl-expr-incexprs (vl-expr-fix x))
         (vl-expr-incexprs x)))

Theorem: vl-exprlist-incexprs-of-vl-exprlist-fix-x

(defthm vl-exprlist-incexprs-of-vl-exprlist-fix-x
  (equal (vl-exprlist-incexprs (vl-exprlist-fix x))
         (vl-exprlist-incexprs x)))

Theorem: vl-expr-incexprs-vl-expr-equiv-congruence-on-x

(defthm vl-expr-incexprs-vl-expr-equiv-congruence-on-x
  (implies (vl-expr-equiv x x-equiv)
           (equal (vl-expr-incexprs x)
                  (vl-expr-incexprs x-equiv)))
  :rule-classes :congruence)

Theorem: vl-exprlist-incexprs-vl-exprlist-equiv-congruence-on-x

(defthm vl-exprlist-incexprs-vl-exprlist-equiv-congruence-on-x
  (implies (vl-exprlist-equiv x x-equiv)
           (equal (vl-exprlist-incexprs x)
                  (vl-exprlist-incexprs x-equiv)))
  :rule-classes :congruence)

Subtopics

Vl-exprlist-incexprs