		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Local-variables

Signature
(local-variables expr) → vars
Returns: vars — Type (typed-variable-listp vars).

Definitions and Theorems

Function: local-variables

(defun local-variables (expr)
  (declare (xargs :guard t))
  (let ((__function__ 'local-variables))
    (declare (ignorable __function__))
    (if (atom expr)
        nil
      (let ((rec-vars (append (local-variables (car expr))
                              (local-variables (cdr expr)))))
        (if (and (expressionp expr)
                 (equal (expression-kind expr) ':bind))
            (append (expression-bind->variables expr)
                    rec-vars)
          rec-vars)))))

Theorem: typed-variable-listp-of-local-variables

(defthm typed-variable-listp-of-local-variables
  (b* ((vars (local-variables expr)))
    (typed-variable-listp vars))
  :rule-classes :rewrite)