		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvars-of-choice-fn

Function variables depended on by a choice second-order function or by an instance of it.

Signature
(funvars-of-choice-fn fun wrld) → funvars
Arguments: fun — Guard (symbolp fun).; wrld — Guard (plist-worldp wrld).
Returns: funvars — A funvar-listp.

Choice second-order functions and their instances may depend on function variables via their defining bodies.

The returned list may contain duplicates.

Definitions and Theorems

Function: funvars-of-choice-fn

(defun funvars-of-choice-fn (fun wrld)
  (declare (xargs :guard (and (symbolp fun)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-choice-fn))
    (declare (ignorable __function__))
    (funvars-of-term (defchoose-body fun wrld)
                     wrld)))