		Search-engine friendly clone of the ACL2 documentation.

Atc-variable-tables

Atc-add-var

Add a variable with some information to the symbol table.

Signature
(atc-add-var var info inscope) → new-inscope
Arguments: var — Guard (symbolp var).; info — Guard (atc-var-infop info).; inscope — Guard (atc-symbol-varinfo-alist-listp inscope).
Returns: new-inscope — Type (atc-symbol-varinfo-alist-listp new-inscope).

This is added to the innermost scope. The symbol table has always at least one scope.

This is always called after checking that that variable is not already in scope (via atc-check-var). So it unconditionally adds the variable without checking first.

Definitions and Theorems

Function: atc-add-var

(defun atc-add-var (var info inscope)
 (declare
      (xargs :guard (and (symbolp var)
                         (atc-var-infop info)
                         (atc-symbol-varinfo-alist-listp inscope))))
 (let ((__function__ 'atc-add-var))
   (declare (ignorable __function__))
   (cons (acons (symbol-fix var)
                (atc-var-info-fix info)
                (atc-symbol-varinfo-alist-fix (car inscope)))
         (atc-symbol-varinfo-alist-list-fix (cdr inscope)))))

Theorem: atc-symbol-varinfo-alist-listp-of-atc-add-var

(defthm atc-symbol-varinfo-alist-listp-of-atc-add-var
  (b* ((new-inscope (atc-add-var var info inscope)))
    (atc-symbol-varinfo-alist-listp new-inscope))
  :rule-classes :rewrite)