		Search-engine friendly clone of the ACL2 documentation.

Execution

Extend-denv-with-fundecl

Extend a dynamic environment with a function declaration.

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

Information about the function is added to the dynamic function environment, unless a function with that name is already present.

Definitions and Theorems

Function: extend-denv-with-fundecl

(defun extend-denv-with-fundecl (decl env)
  (declare (xargs :guard (and (fundeclp decl) (denvp env))))
  (let ((__function__ 'extend-denv-with-fundecl))
    (declare (ignorable __function__))
    (b* (((fundecl decl) decl)
         (info (make-function-dinfo :inputs decl.inputs
                                    :output decl.output
                                    :body decl.body))
         (fenv (denv->functions env))
         (new-fenv (add-function-dinfo decl.name info fenv))
         ((when (function-denv-option-case new-fenv :none))
          (reserrf (list :duplicate-function decl.name)))
         (new-fenv (function-denv-option-some->get new-fenv))
         (new-env (change-denv env :functions new-fenv)))
      new-env)))

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

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

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

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

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

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

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

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

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

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