		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Get-var/const-sinfo

Retrieve information about a variable or constant from a static environment.

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

We return nil if the variable or constant is not found. This includes the case that the identifier is in the environment but it does not refers to a variable or constant.

Definitions and Theorems

Function: get-var/const-sinfo

(defun get-var/const-sinfo (v/c env)
  (declare (xargs :guard (and (identifierp v/c) (senvp env))))
  (let ((__function__ 'get-var/const-sinfo))
    (declare (ignorable __function__))
    (b* ((info (get-ident-sinfo v/c env))
         ((unless info) nil))
      (ident-sinfo-case info
                        :var/const info.get
                        :function nil
                        :struct nil))))

Theorem: var/const-sinfo-optionp-of-get-var/const-sinfo

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

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

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

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

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

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

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

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

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