		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Add-var/const-sinfo

Add information about a variable or constant to a static environment.

Signature
(add-var/const-sinfo v/c info env) → new-env
Arguments: v/c — Guard (identifierp v/c).; info — Guard (var/const-sinfop info).; env — Guard (senvp env).
Returns: new-env — Type (senv-optionp new-env).

We return nil if the identifier is already in the environment.

Definitions and Theorems

Function: add-var/const-sinfo

(defun add-var/const-sinfo (v/c info env)
  (declare (xargs :guard (and (identifierp v/c)
                              (var/const-sinfop info)
                              (senvp env))))
  (let ((__function__ 'add-var/const-sinfo))
    (declare (ignorable __function__))
    (add-ident-sinfo v/c (ident-sinfo-var/const info)
                     env)))

Theorem: senv-optionp-of-add-var/const-sinfo

(defthm senv-optionp-of-add-var/const-sinfo
  (b* ((new-env (add-var/const-sinfo v/c info env)))
    (senv-optionp new-env))
  :rule-classes :rewrite)

Theorem: add-var/const-sinfo-of-identifier-fix-v/c

(defthm add-var/const-sinfo-of-identifier-fix-v/c
  (equal (add-var/const-sinfo (identifier-fix v/c)
                              info env)
         (add-var/const-sinfo v/c info env)))

Theorem: add-var/const-sinfo-identifier-equiv-congruence-on-v/c

(defthm add-var/const-sinfo-identifier-equiv-congruence-on-v/c
  (implies (identifier-equiv v/c v/c-equiv)
           (equal (add-var/const-sinfo v/c info env)
                  (add-var/const-sinfo v/c-equiv info env)))
  :rule-classes :congruence)

Theorem: add-var/const-sinfo-of-var/const-sinfo-fix-info

(defthm add-var/const-sinfo-of-var/const-sinfo-fix-info
  (equal (add-var/const-sinfo v/c (var/const-sinfo-fix info)
                              env)
         (add-var/const-sinfo v/c info env)))

Theorem: add-var/const-sinfo-var/const-sinfo-equiv-congruence-on-info

(defthm add-var/const-sinfo-var/const-sinfo-equiv-congruence-on-info
  (implies (var/const-sinfo-equiv info info-equiv)
           (equal (add-var/const-sinfo v/c info env)
                  (add-var/const-sinfo v/c info-equiv env)))
  :rule-classes :congruence)

Theorem: add-var/const-sinfo-of-senv-fix-env

(defthm add-var/const-sinfo-of-senv-fix-env
  (equal (add-var/const-sinfo v/c info (senv-fix env))
         (add-var/const-sinfo v/c info env)))

Theorem: add-var/const-sinfo-senv-equiv-congruence-on-env

(defthm add-var/const-sinfo-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (add-var/const-sinfo v/c info env)
                  (add-var/const-sinfo v/c info env-equiv)))
  :rule-classes :congruence)