		Search-engine friendly clone of the ACL2 documentation.

Free-vars

Free-vars-decl

Collect free variables appearing in a declaration.

Signature
(free-vars-decl decl bound-vars) → (mv free-vars bound-vars)
Arguments: decl — Guard (declp decl).; bound-vars — Guard (ident-setp bound-vars).
Returns: free-vars — Type (ident-setp free-vars).; bound-vars — Type (ident-setp bound-vars).

Definitions and Theorems

Function: free-vars-decl

(defun free-vars-decl (decl bound-vars)
 (declare (xargs :guard (and (declp decl)
                             (ident-setp bound-vars))))
 (let ((__function__ 'free-vars-decl))
  (declare (ignorable __function__))
  (b* ((bound-vars (ident-set-fix bound-vars)))
   (decl-case decl
              :decl (free-vars-initdeclor-list decl.init bound-vars)
              :statassert (mv nil bound-vars)))))

Theorem: ident-setp-of-free-vars-decl.free-vars

(defthm ident-setp-of-free-vars-decl.free-vars
  (b* (((mv ?free-vars ?bound-vars)
        (free-vars-decl decl bound-vars)))
    (ident-setp free-vars))
  :rule-classes :rewrite)

Theorem: ident-setp-of-free-vars-decl.bound-vars

(defthm ident-setp-of-free-vars-decl.bound-vars
  (b* (((mv ?free-vars ?bound-vars)
        (free-vars-decl decl bound-vars)))
    (ident-setp bound-vars))
  :rule-classes :rewrite)