		Search-engine friendly clone of the ACL2 documentation.

Soft-implementation-core

Sothmp

Recognize second-order theorems.

Signature
(sothmp sothm wrld) → yes/no
Arguments: sothm — Guard (symbolp sothm).; wrld — Guard (plist-worldp wrld).
Returns: yes/no — A booleanp.

A theorem is second-order iff it depends on one or more function variables.

Definitions and Theorems

Function: sothmp

(defun sothmp (sothm wrld)
  (declare (xargs :guard (and (symbolp sothm)
                              (plist-worldp wrld))))
  (let ((__function__ 'sothmp))
    (declare (ignorable __function__))
    (not (null (funvars-of-thm sothm wrld)))))