		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-undo

Signature
(vl-elabindex-undo &key (elabindex 'elabindex)) → new-elabindex

Definitions and Theorems

Function: vl-elabindex-undo-fn

(defun vl-elabindex-undo-fn (elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard t))
  (let ((__function__ 'vl-elabindex-undo))
    (declare (ignorable __function__))
    (b* ((undostack (vl-elabindex->undostack elabindex))
         ((unless (consp undostack))
          (raise "Empty undostack")
          (vl-elabindex-update-undostack nil elabindex))
         ((cons undo ss) (car undostack))
         ((mv scopes &)
          (vl-elabscopes-traverse/update
               undo (vl-elabindex->scopes elabindex)))
         (elabindex (vl-elabindex-update-scopes scopes elabindex))
         (elabindex (vl-elabindex-update-undostack (cdr undostack)
                                                   elabindex)))
      (vl-elabindex-update-ss ss elabindex))))

Theorem: undostack-of-vl-elabindex-undo

(defthm undostack-of-vl-elabindex-undo
  (equal (vl-elabindex->undostack (vl-elabindex-undo))
         (cdr (vl-elabindex->undostack))))