		Search-engine friendly clone of the ACL2 documentation.

Dynamic-environments

Get-var/const-dinfo-from-scope

Get the information about a variable or constant from a scope.

Signature
(get-var/const-dinfo-from-scope name scope) → dinfo
Arguments: name — Guard (identifierp name).; scope — Guard (vcscope-dinfop scope).
Returns: dinfo — Type (var/const-dinfo-optionp dinfo).

We return nil if there is no variable of constant with that name.

Definitions and Theorems

Function: get-var/const-dinfo-from-scope

(defun get-var/const-dinfo-from-scope (name scope)
  (declare (xargs :guard (and (identifierp name)
                              (vcscope-dinfop scope))))
  (let ((__function__ 'get-var/const-dinfo-from-scope))
    (declare (ignorable __function__))
    (cdr (omap::assoc (identifier-fix name)
                      (vcscope-dinfo-fix scope)))))

Theorem: var/const-dinfo-optionp-of-get-var/const-dinfo-from-scope

(defthm var/const-dinfo-optionp-of-get-var/const-dinfo-from-scope
  (b* ((dinfo (get-var/const-dinfo-from-scope name scope)))
    (var/const-dinfo-optionp dinfo))
  :rule-classes :rewrite)

Theorem: get-var/const-dinfo-from-scope-of-identifier-fix-name

(defthm get-var/const-dinfo-from-scope-of-identifier-fix-name
  (equal (get-var/const-dinfo-from-scope (identifier-fix name)
                                         scope)
         (get-var/const-dinfo-from-scope name scope)))

Theorem: get-var/const-dinfo-from-scope-identifier-equiv-congruence-on-name

(defthm
 get-var/const-dinfo-from-scope-identifier-equiv-congruence-on-name
 (implies (identifier-equiv name name-equiv)
          (equal (get-var/const-dinfo-from-scope name scope)
                 (get-var/const-dinfo-from-scope name-equiv scope)))
 :rule-classes :congruence)

Theorem: get-var/const-dinfo-from-scope-of-vcscope-dinfo-fix-scope

(defthm get-var/const-dinfo-from-scope-of-vcscope-dinfo-fix-scope
 (equal
     (get-var/const-dinfo-from-scope name (vcscope-dinfo-fix scope))
     (get-var/const-dinfo-from-scope name scope)))

Theorem: get-var/const-dinfo-from-scope-vcscope-dinfo-equiv-congruence-on-scope

(defthm
 get-var/const-dinfo-from-scope-vcscope-dinfo-equiv-congruence-on-scope
 (implies (vcscope-dinfo-equiv scope scope-equiv)
          (equal (get-var/const-dinfo-from-scope name scope)
                 (get-var/const-dinfo-from-scope name scope-equiv)))
 :rule-classes :congruence)