		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-sync-scopes

Ensure that all parent scopes have the current version of all child scopes. This is accomplished by simply popping up to the root level and then returning to the current scope.

Signature
(vl-elabindex-sync-scopes &key (elabindex 'elabindex)) → new-elabindex

Definitions and Theorems

Function: vl-elabindex-sync-scopes-fn

(defun vl-elabindex-sync-scopes-fn (elabindex)
 (declare (xargs :stobjs (elabindex)))
 (declare (xargs :guard t))
 (let ((__function__ 'vl-elabindex-sync-scopes))
  (declare (ignorable __function__))
  (b*
   ((elabindex
      (vl-elabindex-traverse nil (list (vl-elabinstruction-root)))))
   (vl-elabindex-undo))))

Theorem: undostack-of-vl-elabindex-sync-scopes

(defthm undostack-of-vl-elabindex-sync-scopes
  (b* ((?new-elabindex (vl-elabindex-sync-scopes-fn elabindex)))
    (equal (vl-elabindex->undostack new-elabindex)
           (vl-elabindex->undostack))))