		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Plain-sofunp

Recognize plain second-order functions.

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

Definitions and Theorems

Function: plain-sofunp

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

Theorem: booleanp-of-plain-sofunp

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