Add a block scope to a variable table.
(var-table-add-block vartab) → new-table
We add the empty set (of variables) to the front of the sequence. This is used when a block is entered.
Since a variable table is never empty, as enforced by its invariant, any scope added to it must be a block scope, because the file scope is always in the table.
Function:
(defun var-table-add-block (vartab) (declare (xargs :guard (var-tablep vartab))) (let ((__function__ 'var-table-add-block)) (declare (ignorable __function__)) (cons nil (var-table-fix vartab))))
Theorem:
(defthm var-tablep-of-var-table-add-block (b* ((new-table (var-table-add-block vartab))) (var-tablep new-table)) :rule-classes :rewrite)
Theorem:
(defthm var-table-add-block-of-var-table-fix-vartab (equal (var-table-add-block (var-table-fix vartab)) (var-table-add-block vartab)))
Theorem:
(defthm var-table-add-block-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (var-table-add-block vartab) (var-table-add-block vartab-equiv))) :rule-classes :congruence)