		Search-engine friendly clone of the ACL2 documentation.

Union-env

Union-env-block

Unions two scope blocks.

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

See (tsee union-env).

Definitions and Theorems

Function: union-env-block

(defun union-env-block (x y)
  (declare (xargs :guard (and (env-blockp x) (env-blockp y))))
  (let ((__function__ 'union-env-block))
    (declare (ignorable __function__))
    (if (omap::emptyp x)
        nil
      (b* ((ident (ident-fix (omap::head-key x)))
           (value? (c::value-option-fix (omap::head-val x)))
           (y-lookup (omap::assoc ident y)))
        (if (and y-lookup (equal value? (cdr y-lookup)))
            (omap::update ident value?
                          (union-env-block (omap::tail x) y))
          (union-env-block (omap::tail x) y))))))

Theorem: env-blockp-of-union-env-block

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