Set of free variables in a definition.
(definition-free-vars def) → vars
These are the variables in the body minus the parameters.
Function:
(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:
(defthm string-setp-of-definition-free-vars (b* ((vars (definition-free-vars def))) (string-setp vars)) :rule-classes :rewrite)