		Search-engine friendly clone of the ACL2 documentation.

Static-environments

Get-ident-sinfo

Retrieve information about an identifier from a static environment.

Signature
(get-ident-sinfo id env) → info
Arguments: id — Guard (identifierp id).; env — Guard (senvp env).
Returns: info — Type (ident-sinfo-optionp info).

We return nil if the identifier is not found.

Definitions and Theorems

Function: get-ident-sinfo

(defun get-ident-sinfo (id env)
  (declare (xargs :guard (and (identifierp id) (senvp env))))
  (let ((__function__ 'get-ident-sinfo))
    (declare (ignorable __function__))
    (cdr (omap::assoc (identifier-fix id)
                      (senv->identifiers env)))))

Theorem: ident-sinfo-optionp-of-get-ident-sinfo

(defthm ident-sinfo-optionp-of-get-ident-sinfo
  (b* ((info (get-ident-sinfo id env)))
    (ident-sinfo-optionp info))
  :rule-classes :rewrite)

Theorem: get-ident-sinfo-of-identifier-fix-id

(defthm get-ident-sinfo-of-identifier-fix-id
  (equal (get-ident-sinfo (identifier-fix id)
                          env)
         (get-ident-sinfo id env)))

Theorem: get-ident-sinfo-identifier-equiv-congruence-on-id

(defthm get-ident-sinfo-identifier-equiv-congruence-on-id
  (implies (identifier-equiv id id-equiv)
           (equal (get-ident-sinfo id env)
                  (get-ident-sinfo id-equiv env)))
  :rule-classes :congruence)

Theorem: get-ident-sinfo-of-senv-fix-env

(defthm get-ident-sinfo-of-senv-fix-env
  (equal (get-ident-sinfo id (senv-fix env))
         (get-ident-sinfo id env)))

Theorem: get-ident-sinfo-senv-equiv-congruence-on-env

(defthm get-ident-sinfo-senv-equiv-congruence-on-env
  (implies (senv-equiv env env-equiv)
           (equal (get-ident-sinfo id env)
                  (get-ident-sinfo id env-equiv)))
  :rule-classes :congruence)