		Search-engine friendly clone of the ACL2 documentation.

Dynamic-function-environments

Add-function-dinfo

Add information for a function to a dynamic environment.

Signature
(add-function-dinfo fun info env) → new-env
Arguments: fun — Guard (identifierp fun).; info — Guard (function-dinfop info).; env — Guard (function-denvp env).
Returns: new-env — Type (function-denv-optionp new-env).

We return `none' if there is already a function with the same nme in the environment.

Definitions and Theorems

Function: add-function-dinfo

(defun add-function-dinfo (fun info env)
  (declare (xargs :guard (and (identifierp fun)
                              (function-dinfop info)
                              (function-denvp env))))
  (let ((__function__ 'add-function-dinfo))
    (declare (ignorable __function__))
    (b* ((fun (identifier-fix fun))
         (info (function-dinfo-fix info))
         (env (function-denv-fix env))
         ((when (consp (omap::assoc fun env)))
          (function-denv-option-none))
         (new-env (omap::update fun info env)))
      (function-denv-option-some new-env))))

Theorem: function-denv-optionp-of-add-function-dinfo

(defthm function-denv-optionp-of-add-function-dinfo
  (b* ((new-env (add-function-dinfo fun info env)))
    (function-denv-optionp new-env))
  :rule-classes :rewrite)

Theorem: add-function-dinfo-of-identifier-fix-fun

(defthm add-function-dinfo-of-identifier-fix-fun
  (equal (add-function-dinfo (identifier-fix fun)
                             info env)
         (add-function-dinfo fun info env)))

Theorem: add-function-dinfo-identifier-equiv-congruence-on-fun

(defthm add-function-dinfo-identifier-equiv-congruence-on-fun
  (implies (identifier-equiv fun fun-equiv)
           (equal (add-function-dinfo fun info env)
                  (add-function-dinfo fun-equiv info env)))
  :rule-classes :congruence)

Theorem: add-function-dinfo-of-function-dinfo-fix-info

(defthm add-function-dinfo-of-function-dinfo-fix-info
  (equal (add-function-dinfo fun (function-dinfo-fix info)
                             env)
         (add-function-dinfo fun info env)))

Theorem: add-function-dinfo-function-dinfo-equiv-congruence-on-info

(defthm add-function-dinfo-function-dinfo-equiv-congruence-on-info
  (implies (function-dinfo-equiv info info-equiv)
           (equal (add-function-dinfo fun info env)
                  (add-function-dinfo fun info-equiv env)))
  :rule-classes :congruence)

Theorem: add-function-dinfo-of-function-denv-fix-env

(defthm add-function-dinfo-of-function-denv-fix-env
  (equal (add-function-dinfo fun info (function-denv-fix env))
         (add-function-dinfo fun info env)))

Theorem: add-function-dinfo-function-denv-equiv-congruence-on-env

(defthm add-function-dinfo-function-denv-equiv-congruence-on-env
  (implies (function-denv-equiv env env-equiv)
           (equal (add-function-dinfo fun info env)
                  (add-function-dinfo fun info env-equiv)))
  :rule-classes :congruence)