		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 (string-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: string-setp-of-expression-list-vars

(defthm string-setp-of-expression-list-vars
  (b* ((vars (expression-list-vars exprs)))
    (string-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 (string-list-fix vars))))