		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Quant-sofunp

Recognize quantifier second-order functions.

Signature
(quant-sofunp sofun wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

Definitions and Theorems

Function: quant-sofunp

(defun quant-sofunp (sofun wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'quant-sofunp))
    (declare (ignorable __function__))
    (and (sofunp sofun wrld)
         (eq (sofun-kind sofun wrld) 'quant))))

Theorem: booleanp-of-quant-sofunp

(defthm booleanp-of-quant-sofunp
  (b* ((yes/no (quant-sofunp sofun wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)