		Search-engine friendly clone of the ACL2 documentation.

Merge-block-env

Update the top block of the environment with the specified scope block.

Signature
(merge-block-env block env) → new-env
Arguments: block — Guard (env-blockp block).; env — Guard (envp env).
Returns: new-env — Type (envp new-env).

Definitions and Theorems

Function: merge-block-env

(defun merge-block-env (block env)
  (declare (xargs :guard (and (env-blockp block) (envp env))))
  (let ((__function__ 'merge-block-env))
    (declare (ignorable __function__))
    (b* ((block (env-block-fix block))
         (env (env-fix env))
         ((when (endp env)) nil))
      (cons (omap::update* block (first env))
            (rest env)))))

Theorem: envp-of-merge-block-env

(defthm envp-of-merge-block-env
  (b* ((new-env (merge-block-env block env)))
    (envp new-env))
  :rule-classes :rewrite)