		Search-engine friendly clone of the ACL2 documentation.

Stripping-functions

Vl-expr-strip

Throw away attributes and widths, keeping just the core of an expression. (memoized)

Signature
(vl-expr-strip x) → new-x
Arguments: x — Guard (vl-expr-p x).
Returns: new-x — Type (vl-expr-p new-x).

Note that we gain significant performance in leftright-check by memoizing this function.

Theorem: return-type-of-vl-expr-strip.new-x

(defthm return-type-of-vl-expr-strip.new-x
  (b* ((?new-x (vl-expr-strip x)))
    (vl-expr-p new-x))
  :rule-classes :rewrite)

Theorem: return-type-of-vl-exprlist-strip.new-x

(defthm return-type-of-vl-exprlist-strip.new-x
  (b* ((?new-x (vl-exprlist-strip x)))
    (and (vl-exprlist-p new-x)
         (equal (len new-x) (len x))))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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

Subtopics

Vl-exprlist-strip