		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sof-instances

Known instances of a second-order function.

Signature
(sof-instances sofun wrld) → instmap
Arguments: sofun — Guard (sofunp sofun wrld).; wrld — Guard (plist-worldp wrld).
Returns: instmap — A sof-instancesp.

Definitions and Theorems

Function: sof-instances

(defun sof-instances (sofun wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (sofunp sofun wrld))))
  (let ((__function__ 'sof-instances))
    (declare (ignorable __function__))
    (let ((table (table-alist 'sof-instances wrld)
))
      (cdr (assoc-eq sofun table)))))