		Search-engine friendly clone of the ACL2 documentation.

Expr-simp

Vl-expr-simp

Core routine to simplify expressions.

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

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

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

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

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

Subtopics

Vl-exprlist-simp