		Search-engine friendly clone of the ACL2 documentation.

Type-checking

Extend-senv-with-topdecl-list

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

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

Definitions and Theorems

Function: extend-senv-with-topdecl-list

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

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

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

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

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

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

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

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

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

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

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