		Search-engine friendly clone of the ACL2 documentation.

Push-scope-env

Push a new scope block to the top of the environment.

Signature
(push-scope-env env) → new-env
Arguments: env — Guard (envp env).
Returns: new-env — Type (envp new-env).

This mirrors entering a new scope block in the corresponding C program. Newly declared variables (see declare-var-env) shall be declared within the top scope block.

Definitions and Theorems

Function: push-scope-env

(defun push-scope-env (env)
  (declare (xargs :guard (envp env)))
  (let ((__function__ 'push-scope-env))
    (declare (ignorable __function__))
    (cons nil (env-fix env))))

Theorem: envp-of-push-scope-env

(defthm envp-of-push-scope-env
  (b* ((new-env (push-scope-env env)))
    (envp new-env))
  :rule-classes :rewrite)