		Search-engine friendly clone of the ACL2 documentation.

Free-vars

Free-vars-fundef

Collect free variables appearing in a function function definition.

Signature
(free-vars-fundef fundef bound-vars) → free-vars
Arguments: fundef — Guard (fundefp fundef).; bound-vars — Guard (ident-setp bound-vars).
Returns: free-vars — Type (ident-setp free-vars).

Definitions and Theorems

Function: free-vars-fundef

(defun free-vars-fundef (fundef bound-vars)
  (declare (xargs :guard (and (fundefp fundef)
                              (ident-setp bound-vars))))
  (let ((__function__ 'free-vars-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef)
         ((mv free-vars bound-vars)
          (free-vars-decl-list fundef.decls bound-vars)))
      (union free-vars
             (free-vars-stmt fundef.body bound-vars)))))

Theorem: ident-setp-of-free-vars-fundef

(defthm ident-setp-of-free-vars-fundef
  (b* ((free-vars (free-vars-fundef fundef bound-vars)))
    (ident-setp free-vars))
  :rule-classes :rewrite)