		Search-engine friendly clone of the ACL2 documentation.

Dynamic-function-environments

Get-function-dinfo

Get the information for a function in a dynamic environment.

Signature
(get-function-dinfo fun env) → info?
Arguments: fun — Guard (identifierp fun).; env — Guard (function-denvp env).
Returns: info? — Type (function-dinfo-optionp info?).

If there is no function with that name in the environment, we return nil to indicate an error.

Definitions and Theorems

Function: get-function-dinfo

(defun get-function-dinfo (fun env)
  (declare (xargs :guard (and (identifierp fun)
                              (function-denvp env))))
  (let ((__function__ 'get-function-dinfo))
    (declare (ignorable __function__))
    (cdr (omap::assoc (identifier-fix fun)
                      (function-denv-fix env)))))

Theorem: function-dinfo-optionp-of-get-function-dinfo

(defthm function-dinfo-optionp-of-get-function-dinfo
  (b* ((info? (get-function-dinfo fun env)))
    (function-dinfo-optionp info?))
  :rule-classes :rewrite)

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

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

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

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

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

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

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

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