		Search-engine friendly clone of the ACL2 documentation.

Vl-delta-p

Vl-starting-delta

Build an initial vl-delta-p for the module x.

Signature
(vl-starting-delta x) → delta
Arguments: x — Guard (vl-module-p x).

The new delta has an appropriate starting namefactory for the module, and is also seeded with the module's warnings. The other accumulators are all empty to begin with.

Definitions and Theorems

Function: vl-starting-delta

(defun vl-starting-delta (x)
  (declare (xargs :guard (vl-module-p x)))
  (let ((__function__ 'vl-starting-delta))
    (declare (ignorable __function__))
    (make-vl-delta :nf (vl-starting-namefactory x)
                   :warnings (vl-module->warnings x)
                   :vardecls nil
                   :assigns nil
                   :modinsts nil
                   :addmods nil)))

Theorem: vl-starting-delta-of-vl-module-fix-x

(defthm vl-starting-delta-of-vl-module-fix-x
  (equal (vl-starting-delta (vl-module-fix x))
         (vl-starting-delta x)))

Theorem: vl-starting-delta-vl-module-equiv-congruence-on-x

(defthm vl-starting-delta-vl-module-equiv-congruence-on-x
  (implies (vl-module-equiv x x-equiv)
           (equal (vl-starting-delta x)
                  (vl-starting-delta x-equiv)))
  :rule-classes :congruence)