		Search-engine friendly clone of the ACL2 documentation.

Free-vars

Free-vars-fundef

Collect free variables appearing in a 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))))
 (b* (((fundef fundef) fundef)
      (free-vars1 (free-vars-decl-spec-list fundef.spec bound-vars))
      ((mv free-vars2 bound-vars param-bound-vars)
       (free-vars-declor fundef.declor bound-vars))
      (bound-vars (union bound-vars param-bound-vars))
      (free-vars3
           (free-vars-attrib-spec-list fundef.attribs bound-vars))
      ((mv free-vars4 bound-vars)
       (free-vars-decl-list fundef.decls bound-vars))
      (free-vars5 (free-vars-stmt fundef.body bound-vars)))
   (union free-vars1
          (union free-vars2
                 (union free-vars3
                        (union free-vars4 free-vars5))))))

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)