		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-pop-scope

Pop a scope from the disambiguation table.

Signature
(dimb-pop-scope table) → new-table
Arguments: table — Guard (dimb-tablep table).
Returns: new-table — Type (dimb-tablep new-table).

It is an internal error if the table is empty; it should never be empty. We should replace this with guards and proofs.

We remove the top scope, via cdr. Recall that the stack top is on the left; see dimb-push-scope.

Definitions and Theorems

Function: dimb-pop-scope

(defun dimb-pop-scope (table)
  (declare (xargs :guard (dimb-tablep table)))
  (let ((__function__ 'dimb-pop-scope))
    (declare (ignorable __function__))
    (if (consp table)
        (dimb-table-fix (cdr table))
      (raise "Internal error: empty disambiguation table."))))

Theorem: dimb-tablep-of-dimb-pop-scope

(defthm dimb-tablep-of-dimb-pop-scope
  (b* ((new-table (dimb-pop-scope table)))
    (dimb-tablep new-table))
  :rule-classes :rewrite)

Theorem: dimb-pop-scope-of-dimb-table-fix-table

(defthm dimb-pop-scope-of-dimb-table-fix-table
  (equal (dimb-pop-scope (dimb-table-fix table))
         (dimb-pop-scope table)))

Theorem: dimb-pop-scope-dimb-table-equiv-congruence-on-table

(defthm dimb-pop-scope-dimb-table-equiv-congruence-on-table
  (implies (dimb-table-equiv table table-equiv)
           (equal (dimb-pop-scope table)
                  (dimb-pop-scope table-equiv)))
  :rule-classes :congruence)