		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sofun-funvars

Function variables that a second-order function depends on.

Signature
(sofun-funvars sofun wrld) → funvars
Arguments: sofun — Guard (sofunp sofun wrld).; wrld — Guard (plist-worldp wrld).
Returns: funvars — A funvar-listp.

Definitions and Theorems

Function: sofun-funvars

(defun sofun-funvars (sofun wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (sofunp sofun wrld))))
  (let ((__function__ 'sofun-funvars))
    (declare (ignorable __function__))
    (let ((table (table-alist 'second-order-functions
                              wrld)
))
      (cdr (assoc-eq sofun table)))))