		Search-engine friendly clone of the ACL2 documentation.

Union-env

Take the conservative union of two environments.

Signature
(union-env x y) → env
Arguments: x — Guard (envp x).; y — Guard (envp y).
Returns: env — Type (envp env).

It is assumed that the each scope block in the environment agrees on which variables have been declared. They may only disagree on the value of variables

For each scope block, the value of variables which are agreed upon by the two environment are retained. The values of all other variables are marked "unknown".

Definitions and Theorems

Function: union-env

(defun union-env (x y)
  (declare (xargs :guard (and (envp x) (envp y))))
  (let ((__function__ 'union-env))
    (declare (ignorable __function__))
    (if (endp x)
        nil
      (cons (union-env-block (first x) (first y))
            (union-env (rest x) (rest y))))))

Theorem: envp-of-union-env

(defthm envp-of-union-env
  (b* ((env (union-env x y))) (envp env))
  :rule-classes :rewrite)

Subtopics

Union-env-block: Unions two scope blocks.