		Search-engine friendly clone of the ACL2 documentation.

Disambiguator

Dimb-push-scope

Push a scope into the disambiguation table.

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

We add an empty scope. The top of the stack is on the left, so we push via cons. Also see dimb-pop-scope.

Definitions and Theorems

Function: dimb-push-scope

(defun dimb-push-scope (table)
  (declare (xargs :guard (dimb-tablep table)))
  (let ((__function__ 'dimb-push-scope))
    (declare (ignorable __function__))
    (cons nil (dimb-table-fix table))))

Theorem: dimb-tablep-of-dimb-push-scope

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

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

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

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

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