		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Expression-vars

Set of variables in an expression.

Signature
(expression-vars expr) → vars
Arguments: expr — Guard (expressionp expr).
Returns: vars — Type (string-setp vars).

Definitions and Theorems

Function: expression-vars

(defun expression-vars (expr)
  (declare (xargs :guard (expressionp expr)))
  (let ((__function__ 'expression-vars))
    (declare (ignorable __function__))
    (expression-case expr
                     :const nil
                     :var (insert expr.name nil)
                     :add (union (expression-vars expr.arg1)
                                 (expression-vars expr.arg2))
                     :mul (union (expression-vars expr.arg1)
                                 (expression-vars expr.arg2)))))

Theorem: string-setp-of-expression-vars

(defthm string-setp-of-expression-vars
  (b* ((vars (expression-vars expr)))
    (string-setp vars))
  :rule-classes :rewrite)