		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-pop/update

Signature
(vl-elabscopes-pop/update n scopes) → (mv new-scopes undo)
Arguments: n — Guard (natp n).; scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).; undo — First instruction corresponds to the first scope popped. Therefore, this is a reversed elabpath that reverses this pop operation.
Type (vl-elabtraversal-p undo).

Definitions and Theorems

Function: vl-elabscopes-pop/update

(defun vl-elabscopes-pop/update (n scopes)
  (declare (xargs :guard (and (natp n)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-pop/update))
    (declare (ignorable __function__))
    (if (zp n)
        (mv (vl-elabscopes-fix scopes) nil)
      (b* (((mv scopes undo1)
            (vl-elabscopes-pop/update-one scopes))
           ((mv scopes undo2)
            (vl-elabscopes-pop/update (1- n)
                                      scopes)))
        (mv scopes
            (vl-elabpaths-append undo1 undo2))))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-pop/update.new-scopes

(defthm vl-elabscopes-p-of-vl-elabscopes-pop/update.new-scopes
  (b* (((mv ?new-scopes ?undo)
        (vl-elabscopes-pop/update n scopes)))
    (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabtraversal-p-of-vl-elabscopes-pop/update.undo

(defthm vl-elabtraversal-p-of-vl-elabscopes-pop/update.undo
  (b* (((mv ?new-scopes ?undo)
        (vl-elabscopes-pop/update n scopes)))
    (vl-elabtraversal-p undo))
  :rule-classes :rewrite)

Theorem: vl-elabscopes-pop/update-of-nfix-n

(defthm vl-elabscopes-pop/update-of-nfix-n
  (equal (vl-elabscopes-pop/update (nfix n)
                                   scopes)
         (vl-elabscopes-pop/update n scopes)))

Theorem: vl-elabscopes-pop/update-nat-equiv-congruence-on-n

(defthm vl-elabscopes-pop/update-nat-equiv-congruence-on-n
  (implies (acl2::nat-equiv n n-equiv)
           (equal (vl-elabscopes-pop/update n scopes)
                  (vl-elabscopes-pop/update n-equiv scopes)))
  :rule-classes :congruence)

Theorem: vl-elabscopes-pop/update-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-pop/update-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-pop/update n (vl-elabscopes-fix scopes))
         (vl-elabscopes-pop/update n scopes)))

Theorem: vl-elabscopes-pop/update-vl-elabscopes-equiv-congruence-on-scopes

(defthm
  vl-elabscopes-pop/update-vl-elabscopes-equiv-congruence-on-scopes
  (implies (vl-elabscopes-equiv scopes scopes-equiv)
           (equal (vl-elabscopes-pop/update n scopes)
                  (vl-elabscopes-pop/update n scopes-equiv)))
  :rule-classes :congruence)