		Search-engine friendly clone of the ACL2 documentation.

Std/system/term-queries

All-free/bound-vars

Return all the free and bound variables that occur in a term.

Signature
(all-free/bound-vars term) → vars
Arguments: term — Guard (pseudo-termp term).
Returns: vars — Type (symbol-listp vars), given the guard.

The returned list of variables is in no particular order, but it has no duplicates, because we use union-eq to join variable lists.

This utility is in contrast with the built-in all-vars, which returns only the free variables.

Function: all-free/bound-vars

(defun all-free/bound-vars (term)
 (declare (xargs :guard (pseudo-termp term)))
 (let ((__function__ 'all-free/bound-vars))
  (declare (ignorable __function__))
  (cond
   ((variablep term) (list term))
   ((fquotep term) nil)
   (t
    (b*
     ((fn/lambda (ffn-symb term))
      (fn/lambda-vars
       (and
          (flambdap fn/lambda)
          (union-eq (lambda-formals fn/lambda)
                    (all-free/bound-vars (lambda-body fn/lambda)))))
      (args-vars (all-free/bound-vars-lst (fargs term))))
     (union-eq fn/lambda-vars args-vars))))))

Function: all-free/bound-vars-lst

(defun all-free/bound-vars-lst (terms)
  (declare (xargs :guard (pseudo-term-listp terms)))
  (let ((__function__ 'all-free/bound-vars-lst))
    (declare (ignorable __function__))
    (cond ((endp terms) nil)
          (t (union-eq (all-free/bound-vars (car terms))
                       (all-free/bound-vars-lst (cdr terms)))))))

Theorem: return-type-of-all-free/bound-vars.vars

(defthm return-type-of-all-free/bound-vars.vars
  (implies (and (pseudo-termp term))
           (b* ((?vars (all-free/bound-vars term)))
             (symbol-listp vars)))
  :rule-classes :rewrite)

Theorem: return-type-of-all-free/bound-vars-lst.vars

(defthm return-type-of-all-free/bound-vars-lst.vars
  (implies (and (pseudo-term-listp terms))
           (b* ((?vars (all-free/bound-vars-lst terms)))
             (symbol-listp vars)))
  :rule-classes :rewrite)

Subtopics

All-free/bound-vars-lst