		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sofun-kindp

Recognize symbols that denote the kinds of second-order functions supported by SOFT.

Signature
(sofun-kindp kind) → yes/no
Returns: yes/no — Type (booleanp yes/no).

Following the terminology used in the Workshop paper, in the implementation we use:

plain for second-order functions introduced via defun2.
choice for second-order functions introduced via defchoose2.
quant for second-order functions introduced via defun-sk2.

Definitions and Theorems

Function: sofun-kindp

(defun sofun-kindp (kind)
  (declare (xargs :guard t))
  (let ((__function__ 'sofun-kindp))
    (declare (ignorable __function__))
    (or (eq kind 'plain)
        (eq kind 'choice)
        (eq kind 'quant))))

Theorem: booleanp-of-sofun-kindp

(defthm booleanp-of-sofun-kindp
  (b* ((yes/no (sofun-kindp kind)))
    (booleanp yes/no))
  :rule-classes :rewrite)