		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sofun-kind

Kind of a second-order function.

Signature
(sofun-kind sofun wrld) → kind
Arguments: sofun — Guard (sofunp sofun wrld).; wrld — Guard (plist-worldp wrld).
Returns: kind — A sofun-kindp.

Definitions and Theorems

Function: sofun-kind

(defun sofun-kind (sofun wrld)
  (declare (xargs :guard (and (plist-worldp wrld)
                              (sofunp sofun wrld))))
  (let ((__function__ 'sofun-kind))
    (declare (ignorable __function__))
    (cond ((defchoosep sofun wrld) 'choice)
          ((defun-sk-p sofun wrld) 'quant)
          (t 'plain))))