		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Add-function-sinfo

Add information about a function to a static environment.

Signature
(add-function-sinfo fun info env) → new-env
Arguments: fun — Guard (identifierp fun).; info — Guard (function-sinfop info).; env — Guard (senvp env).
Returns: new-env — Type (senv-optionp new-env).

Definitions and Theorems

Function: add-function-sinfo

(defun add-function-sinfo (fun info env)
  (declare (xargs :guard (and (identifierp fun)
                              (function-sinfop info)
                              (senvp env))))
  (let ((__function__ 'add-function-sinfo))
    (declare (ignorable __function__))
    (add-ident-sinfo fun (ident-sinfo-function info)
                     env)))

Theorem: senv-optionp-of-add-function-sinfo

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

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

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

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

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

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

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

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

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

Theorem: add-function-sinfo-of-senv-fix-env

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

Theorem: add-function-sinfo-senv-equiv-congruence-on-env

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