		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expression-list-vars

Set of variables in a list of expressions.

Signature
(expression-list-vars exprs) → vars
Arguments: exprs — Guard (expression-listp exprs).
Returns: vars — Type (name-setp vars).

Definitions and Theorems

Function: expression-list-vars

(defun expression-list-vars (exprs)
  (declare (xargs :guard (expression-listp exprs)))
  (let ((__function__ 'expression-list-vars))
    (declare (ignorable __function__))
    (cond ((endp exprs) nil)
          (t (union (expression-vars (car exprs))
                    (expression-list-vars (cdr exprs)))))))

Theorem: name-setp-of-expression-list-vars

(defthm name-setp-of-expression-list-vars
  (b* ((vars (expression-list-vars exprs)))
    (name-setp vars))
  :rule-classes :rewrite)

Theorem: expression-list-vars-of-expression-var-list

(defthm expression-list-vars-of-expression-var-list
  (equal (expression-list-vars (expression-var-list vars))
         (mergesort (name-list-fix vars))))

Theorem: expression-list-vars-of-cons

(defthm expression-list-vars-of-cons
  (equal (expression-list-vars (cons expr exprs))
         (union (expression-vars expr)
                (expression-list-vars exprs))))

Theorem: expression-list-vars-of-append

(defthm expression-list-vars-of-append
  (equal (expression-list-vars (append exprs1 exprs2))
         (union (expression-list-vars exprs1)
                (expression-list-vars exprs2))))