		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Definition-free-vars

Set of free variables in a definition.

Signature
(definition-free-vars def) → vars
Arguments: def — Guard (definitionp def).
Returns: vars — Type (string-setp vars).

These are the variables in the body minus the parameters.

Definitions and Theorems

Function: definition-free-vars

(defun definition-free-vars (def)
  (declare (xargs :guard (definitionp def)))
  (let ((__function__ 'definition-free-vars))
    (declare (ignorable __function__))
    (difference (constraint-list-vars (definition->body def))
                (mergesort (definition->para def)))))

Theorem: string-setp-of-definition-free-vars

(defthm string-setp-of-definition-free-vars
  (b* ((vars (definition-free-vars def)))
    (string-setp vars))
  :rule-classes :rewrite)