Function variables that terms depend on.
A term may depend on a function variable directly (when the function variable occurs in the term) or indirectly (when a the second-order function that occurs in the term depends on the function variable).
Note that, in the following code,
if
The returned list may contain duplicates.
Function:
(defun funvars-of-term (term wrld) (declare (xargs :guard (and (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'funvars-of-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) nil (let* ((fn (fn-symb term)) (fn-vars (if (flambdap fn) (funvars-of-term (lambda-body fn) wrld) (if (funvarp fn wrld) (list fn) (if (sofunp fn wrld) (sofun-funvars fn wrld) nil))))) (append fn-vars (funvars-of-terms (fargs term) wrld))))))
Function:
(defun funvars-of-terms (terms wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (plist-worldp wrld)))) (let ((__function__ 'funvars-of-terms)) (declare (ignorable __function__)) (if (endp terms) nil (append (funvars-of-term (car terms) wrld) (funvars-of-terms (cdr terms) wrld)))))
Function:
(defun funvars-of-term (term wrld) (declare (xargs :guard (and (pseudo-termp term) (plist-worldp wrld)))) (let ((__function__ 'funvars-of-term)) (declare (ignorable __function__)) (if (or (variablep term) (quotep term)) nil (let* ((fn (fn-symb term)) (fn-vars (if (flambdap fn) (funvars-of-term (lambda-body fn) wrld) (if (funvarp fn wrld) (list fn) (if (sofunp fn wrld) (sofun-funvars fn wrld) nil))))) (append fn-vars (funvars-of-terms (fargs term) wrld))))))
Function:
(defun funvars-of-terms (terms wrld) (declare (xargs :guard (and (pseudo-term-listp terms) (plist-worldp wrld)))) (let ((__function__ 'funvars-of-terms)) (declare (ignorable __function__)) (if (endp terms) nil (append (funvars-of-term (car terms) wrld) (funvars-of-terms (cdr terms) wrld)))))