		Search-engine friendly clone of the ACL2 documentation.

Elabindex

Vl-elabscopes-pop

Signature
(vl-elabscopes-pop n scopes &key (allow-empty 'nil)) → new-scopes
Arguments: n — Guard (natp n).; scopes — Guard (vl-elabscopes-p scopes).
Returns: new-scopes — Type (vl-elabscopes-p new-scopes).

Definitions and Theorems

Function: vl-elabscopes-pop-fn

(defun vl-elabscopes-pop-fn (n scopes allow-empty)
  (declare (xargs :guard (and (natp n)
                              (vl-elabscopes-p scopes))))
  (let ((__function__ 'vl-elabscopes-pop))
    (declare (ignorable __function__))
    (b* ((scopes (vl-elabscopes-fix scopes)))
      (if (< (lnfix n) (len scopes))
          (nthcdr n scopes)
        (and (not allow-empty)
             (raise "Can't pop ~x0 levels -- only exist ~x1"
                    n (len scopes)))))))

Theorem: vl-elabscopes-p-of-vl-elabscopes-pop

(defthm vl-elabscopes-p-of-vl-elabscopes-pop
  (b* ((new-scopes (vl-elabscopes-pop-fn n scopes allow-empty)))
    (vl-elabscopes-p new-scopes))
  :rule-classes :rewrite)

Theorem: vl-elabscopes-pop-fn-of-nfix-n

(defthm vl-elabscopes-pop-fn-of-nfix-n
  (equal (vl-elabscopes-pop-fn (nfix n)
                               scopes allow-empty)
         (vl-elabscopes-pop-fn n scopes allow-empty)))

Theorem: vl-elabscopes-pop-fn-nat-equiv-congruence-on-n

(defthm vl-elabscopes-pop-fn-nat-equiv-congruence-on-n
 (implies (acl2::nat-equiv n n-equiv)
          (equal (vl-elabscopes-pop-fn n scopes allow-empty)
                 (vl-elabscopes-pop-fn n-equiv scopes allow-empty)))
 :rule-classes :congruence)

Theorem: vl-elabscopes-pop-fn-of-vl-elabscopes-fix-scopes

(defthm vl-elabscopes-pop-fn-of-vl-elabscopes-fix-scopes
  (equal (vl-elabscopes-pop-fn n (vl-elabscopes-fix scopes)
                               allow-empty)
         (vl-elabscopes-pop-fn n scopes allow-empty)))

Theorem: vl-elabscopes-pop-fn-vl-elabscopes-equiv-congruence-on-scopes

(defthm
      vl-elabscopes-pop-fn-vl-elabscopes-equiv-congruence-on-scopes
 (implies (vl-elabscopes-equiv scopes scopes-equiv)
          (equal (vl-elabscopes-pop-fn n scopes allow-empty)
                 (vl-elabscopes-pop-fn n scopes-equiv allow-empty)))
 :rule-classes :congruence)