		Search-engine friendly clone of the ACL2 documentation.

Lint-stmt-rewrite

Vl-lint-stmt-rewrite

Main rewrite. Recursively convert any throwaway statements into null statements.

Signature
(vl-lint-stmt-rewrite x) → new-x
Arguments: x — Guard (vl-stmt-p x).
Returns: new-x — Type (vl-stmt-p new-x).

Theorem: return-type-of-vl-lint-stmt-rewrite.new-x

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

Theorem: return-type-of-vl-lint-stmtlist-rewrite.new-x

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

Subtopics

Vl-lint-stmtlist-rewrite