		Search-engine friendly clone of the ACL2 documentation.

Atc-variable-tables

Atc-get-var

Obtain the information for a variable from the symbol table.

Signature
(atc-get-var var inscope) → info?
Arguments: var — Guard (symbolp var).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).
Returns: info? — Type (atc-var-info-optionp info?).

We look through the scopes, from innermost to outermost. Actually, currently it is an invariant that the scopes are disjoint, so any lookup order would give the same result.

Return nil if the variable is not in scope.

Definitions and Theorems

Function: atc-get-var

(defun atc-get-var (var inscope)
 (declare
      (xargs :guard (and (symbolp var)
                         (atc-symbol-varinfo-alist-listp inscope))))
 (let ((__function__ 'atc-get-var))
  (declare (ignorable __function__))
  (if (endp inscope)
      nil
   (or (cdr (assoc-eq var
                      (atc-symbol-varinfo-alist-fix (car inscope))))
       (atc-get-var var (cdr inscope))))))

Theorem: atc-var-info-optionp-of-atc-get-var

(defthm atc-var-info-optionp-of-atc-get-var
  (b* ((info? (atc-get-var var inscope)))
    (atc-var-info-optionp info?))
  :rule-classes :rewrite)