		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabindex-traverse-undo-entry

Signature
(vl-elabindex-traverse-undo-entry path &key (elabindex 'elabindex)) → undo-entry
Arguments: path — Guard (vl-elabtraversal-p path).
Returns: undo-entry — Type (and (vl-elabtraversal-p (car undo-entry)) (vl-scopestack-p (cdr undo-entry))) .

Definitions and Theorems

Function: vl-elabindex-traverse-undo-entry-fn

(defun vl-elabindex-traverse-undo-entry-fn (path elabindex)
  (declare (xargs :stobjs (elabindex)))
  (declare (xargs :guard (vl-elabtraversal-p path)))
  (let ((__function__ 'vl-elabindex-traverse-undo-entry))
    (declare (ignorable __function__))
    (b* (((mv ?scopes rev-undo)
          (vl-elabscopes-traverse/update
               path (vl-elabindex->scopes elabindex))))
      (cons (rev rev-undo)
            (vl-elabindex->ss)))))

Theorem: return-type-of-vl-elabindex-traverse-undo-entry

(defthm return-type-of-vl-elabindex-traverse-undo-entry
  (b* ((undo-entry
            (vl-elabindex-traverse-undo-entry-fn path elabindex)))
    (and (vl-elabtraversal-p (car undo-entry))
         (vl-scopestack-p (cdr undo-entry))))
  :rule-classes :rewrite)

Theorem: undostack-of-vl-elabindex-traverse

(defthm undostack-of-vl-elabindex-traverse
  (equal (vl-elabindex->undostack (vl-elabindex-traverse ss path))
         (cons (vl-elabindex-traverse-undo-entry path)
               (vl-elabindex->undostack))))

Theorem: vl-elabindex-traverse-undo-entry-fn-of-vl-elabtraversal-fix-path

(defthm
   vl-elabindex-traverse-undo-entry-fn-of-vl-elabtraversal-fix-path
 (equal
    (vl-elabindex-traverse-undo-entry-fn (vl-elabtraversal-fix path)
                                         elabindex)
    (vl-elabindex-traverse-undo-entry-fn path elabindex)))

Theorem: vl-elabindex-traverse-undo-entry-fn-vl-elabtraversal-equiv-congruence-on-path

(defthm
 vl-elabindex-traverse-undo-entry-fn-vl-elabtraversal-equiv-congruence-on-path
 (implies
   (vl-elabtraversal-equiv path path-equiv)
   (equal
        (vl-elabindex-traverse-undo-entry-fn path elabindex)
        (vl-elabindex-traverse-undo-entry-fn path-equiv elabindex)))
 :rule-classes :congruence)