		Search-engine friendly clone of the ACL2 documentation.

Free-vars

Free-vars-initdeclor

Collect free variables appearing in an initializer declarator.

Signature
(free-vars-initdeclor initdeclor bound-vars) → (mv free-vars bound-vars)
Arguments: initdeclor — Guard (initdeclorp initdeclor).; 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-initdeclor

(defun free-vars-initdeclor (initdeclor bound-vars)
  (declare (xargs :guard (and (initdeclorp initdeclor)
                              (ident-setp bound-vars))))
  (let ((__function__ 'free-vars-initdeclor))
    (declare (ignorable __function__))
    (b* ((bound-vars (ident-set-fix bound-vars))
         ((initdeclor initdeclor) initdeclor)
         (ident (declor-get-ident initdeclor.declor)))
      (mv (free-vars-initer-option initdeclor.init? bound-vars)
          (if ident (insert (ident-fix ident) bound-vars)
            bound-vars)))))

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

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

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

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