		Search-engine friendly clone of the ACL2 documentation.

Stmtrewrite

Vl-initial-stmtrewrite

Signature
(vl-initial-stmtrewrite x unroll-limit warnings) → (mv warnings new-x)
Arguments: x — Guard (vl-initial-p x).; unroll-limit — Guard (natp unroll-limit).; warnings — Guard (vl-warninglist-p warnings).
Returns: warnings — Type (vl-warninglist-p warnings), given the guard.; new-x — Type (vl-initial-p new-x), given the guard.

Definitions and Theorems

Function: vl-initial-stmtrewrite

(defun vl-initial-stmtrewrite (x unroll-limit warnings)
  (declare (xargs :guard (and (vl-initial-p x)
                              (natp unroll-limit)
                              (vl-warninglist-p warnings))))
  (let ((__function__ 'vl-initial-stmtrewrite))
    (declare (ignorable __function__))
    (b* (((mv warnings stmt)
          (vl-stmt-rewrite-top (vl-initial->stmt x)
                               unroll-limit warnings))
         (x-prime (change-vl-initial x :stmt stmt)))
      (mv warnings x-prime))))

Theorem: vl-warninglist-p-of-vl-initial-stmtrewrite.warnings

(defthm vl-warninglist-p-of-vl-initial-stmtrewrite.warnings
  (implies (and (force (vl-initial-p x))
                (force (natp unroll-limit))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?new-x)
                 (vl-initial-stmtrewrite x unroll-limit warnings)))
             (vl-warninglist-p warnings)))
  :rule-classes :rewrite)

Theorem: vl-initial-p-of-vl-initial-stmtrewrite.new-x

(defthm vl-initial-p-of-vl-initial-stmtrewrite.new-x
  (implies (and (force (vl-initial-p x))
                (force (natp unroll-limit))
                (force (vl-warninglist-p warnings)))
           (b* (((mv ?warnings ?new-x)
                 (vl-initial-stmtrewrite x unroll-limit warnings)))
             (vl-initial-p new-x)))
  :rule-classes :rewrite)