		Search-engine friendly clone of the ACL2 documentation.

Atc-variable-tables

Atc-get-vars

Lift atc-get-var to lists.

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

Definitions and Theorems

Function: atc-get-vars

(defun atc-get-vars (vars inscope)
 (declare
      (xargs :guard (and (symbol-listp vars)
                         (atc-symbol-varinfo-alist-listp inscope))))
 (let ((__function__ 'atc-get-vars))
   (declare (ignorable __function__))
   (cond ((endp vars) nil)
         (t (cons (atc-get-var (car vars) inscope)
                  (atc-get-vars (cdr vars) inscope))))))

Theorem: atc-var-info-option-listp-of-atc-get-vars

(defthm atc-var-info-option-listp-of-atc-get-vars
  (b* ((info?-list (atc-get-vars vars inscope)))
    (atc-var-info-option-listp info?-list))
  :rule-classes :rewrite)