Collect free variables appearing in a list of declarations.
(free-vars-decl-list decls bound-vars) → (mv free-vars bound-vars)
Function:
(defun free-vars-decl-list (decls bound-vars) (declare (xargs :guard (and (decl-listp decls) (ident-setp bound-vars)))) (let ((__function__ 'free-vars-decl-list)) (declare (ignorable __function__)) (b* ((bound-vars (ident-set-fix bound-vars)) ((when (endp decls)) (mv nil bound-vars)) ((mv free-vars1 bound-vars) (free-vars-decl (first decls) bound-vars)) ((mv free-vars2 bound-vars) (free-vars-decl-list (rest decls) bound-vars))) (mv (union free-vars1 free-vars2) bound-vars))))
Theorem:
(defthm ident-setp-of-free-vars-decl-list.free-vars (b* (((mv ?free-vars ?bound-vars) (free-vars-decl-list decls bound-vars))) (ident-setp free-vars)) :rule-classes :rewrite)
Theorem:
(defthm ident-setp-of-free-vars-decl-list.bound-vars (b* (((mv ?free-vars ?bound-vars) (free-vars-decl-list decls bound-vars))) (ident-setp bound-vars)) :rule-classes :rewrite)