Function variables depended on by a plain second-order function or by an instance of it.
(funvars-of-plain-fn fun wrld) → funvars
Plain second-order functions and their instances may depend on function variables via their defining bodies, via their measures (absent in non-recursive functions), and via their guards. For now recursive second-order functions (which are all plain) and their instances are only allowed to use o< as their well-founded relation, and so plain second-order functions and their instances may not depend on function variables via their well-founded relations.
Note that if the function is recursive,
the variable
The returned list may contain duplicates.
Function:
(defun funvars-of-plain-fn (fun wrld) (declare (xargs :guard (and (symbolp fun) (plist-worldp wrld)))) (let ((__function__ 'funvars-of-plain-fn)) (declare (ignorable __function__)) (let* ((body (ubody fun wrld)) (measure (if (recursivep fun nil wrld) (measure fun wrld) nil)) (guard (uguard fun wrld)) (body-funvars (funvars-of-term body wrld)) (measure-funvars (funvars-of-term measure wrld)) (guard-funvars (funvars-of-term guard wrld))) (append body-funvars measure-funvars guard-funvars))))