		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-init

Signature
(vl-elabindex-init x &key (elabindex 'elabindex)) → new-elabindex
Arguments: x — Guard (vl-design-p x).

Definitions and Theorems

Function: vl-elabindex-init-fn

(defun vl-elabindex-init-fn (x elabindex)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard (vl-design-p x)))
 (let ((__function__ 'vl-elabindex-init))
  (declare (ignorable __function__))
  (b* ((elabindex (vl-elabindex-update-ss (vl-scopestack-init x)
                                          elabindex)))
   (vl-elabindex-update-scopes (list (cons nil (make-vl-elabscope)))
                               elabindex))))

Theorem: undostack-of-vl-elabindex-init

(defthm undostack-of-vl-elabindex-init
  (equal (vl-elabindex->undostack (vl-elabindex-init x))
         (vl-elabindex->undostack)))

Theorem: vl-elabindex-init-fn-of-vl-design-fix-x

(defthm vl-elabindex-init-fn-of-vl-design-fix-x
  (equal (vl-elabindex-init-fn (vl-design-fix x)
                               elabindex)
         (vl-elabindex-init-fn x elabindex)))

Theorem: vl-elabindex-init-fn-vl-design-equiv-congruence-on-x

(defthm vl-elabindex-init-fn-vl-design-equiv-congruence-on-x
  (implies (vl-design-equiv x x-equiv)
           (equal (vl-elabindex-init-fn x elabindex)
                  (vl-elabindex-init-fn x-equiv elabindex)))
  :rule-classes :congruence)