		Search-engine friendly clone of the ACL2 documentation.

Execution

Extend-denv-with-topdecl-list

Extend a dynamic environment with a list of top-level declarations.

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

Definitions and Theorems

Function: extend-denv-with-topdecl-list

(defun extend-denv-with-topdecl-list (decls env)
  (declare (xargs :guard (and (topdecl-listp decls)
                              (denvp env))))
  (let ((__function__ 'extend-denv-with-topdecl-list))
    (declare (ignorable __function__))
    (b* (((when (endp decls)) (denv-fix env))
         ((okf env)
          (extend-denv-with-topdecl (car decls)
                                    env)))
      (extend-denv-with-topdecl-list (cdr decls)
                                     env))))

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

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

Theorem: extend-denv-with-topdecl-list-of-topdecl-list-fix-decls

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

Theorem: extend-denv-with-topdecl-list-topdecl-list-equiv-congruence-on-decls

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

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

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

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

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