		Search-engine friendly clone of the ACL2 documentation.

Execution

Extend-denv-with-topdecl

Extend a dynamic environment with a top-level declaration.

Signature
(extend-denv-with-topdecl decl env) → new-env
Arguments: decl — Guard (topdeclp decl).; env — Guard (denvp env).
Returns: new-env — Type (denv-resultp new-env).

Definitions and Theorems

Function: extend-denv-with-topdecl

(defun extend-denv-with-topdecl (decl env)
  (declare (xargs :guard (and (topdeclp decl) (denvp env))))
  (let ((__function__ 'extend-denv-with-topdecl))
    (declare (ignorable __function__))
    (topdecl-case
         decl
         :function (extend-denv-with-fundecl decl.get env)
         :struct (extend-denv-with-structdecl decl.get env)
         :mapping
         (reserrf :extend-denv-for-mapping-not-yet-implemented))))

Theorem: denv-resultp-of-extend-denv-with-topdecl

(defthm denv-resultp-of-extend-denv-with-topdecl
  (b* ((new-env (extend-denv-with-topdecl decl env)))
    (denv-resultp new-env))
  :rule-classes :rewrite)

Theorem: extend-denv-with-topdecl-of-topdecl-fix-decl

(defthm extend-denv-with-topdecl-of-topdecl-fix-decl
  (equal (extend-denv-with-topdecl (topdecl-fix decl)
                                   env)
         (extend-denv-with-topdecl decl env)))

Theorem: extend-denv-with-topdecl-topdecl-equiv-congruence-on-decl

(defthm extend-denv-with-topdecl-topdecl-equiv-congruence-on-decl
  (implies (topdecl-equiv decl decl-equiv)
           (equal (extend-denv-with-topdecl decl env)
                  (extend-denv-with-topdecl decl-equiv env)))
  :rule-classes :congruence)

Theorem: extend-denv-with-topdecl-of-denv-fix-env

(defthm extend-denv-with-topdecl-of-denv-fix-env
  (equal (extend-denv-with-topdecl decl (denv-fix env))
         (extend-denv-with-topdecl decl env)))

Theorem: extend-denv-with-topdecl-denv-equiv-congruence-on-env

(defthm extend-denv-with-topdecl-denv-equiv-congruence-on-env
  (implies (denv-equiv env env-equiv)
           (equal (extend-denv-with-topdecl decl env)
                  (extend-denv-with-topdecl decl env-equiv)))
  :rule-classes :congruence)