		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Funvars-of-thm

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

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

Second-order theorems and their instances may depend on function variables via their formulas.

The returned list may contain duplicates.

Definitions and Theorems

Function: funvars-of-thm

(defun funvars-of-thm (thm wrld)
  (declare (xargs :guard (and (symbolp thm)
                              (plist-worldp wrld))))
  (let ((__function__ 'funvars-of-thm))
    (declare (ignorable __function__))
    (funvars-of-term (formula thm nil wrld)
                     wrld)))