		Search-engine friendly clone of the ACL2 documentation.

Std/system/event-name-queries

Theorem-namep

Recognize symbols that name theorems.

Signature
(theorem-namep x wrld) → yes/no
Arguments: wrld — Guard (plist-worldp wrld).
Returns: yes/no — Type (booleanp yes/no).

This function is enabled because it is meant as an abbreviation. Thus, theorems triggered by this function should be generally avoided.

Definitions and Theorems

Function: theorem-namep

(defun theorem-namep (x wrld)
  (declare (xargs :guard (plist-worldp wrld)))
  (let ((__function__ 'theorem-namep))
    (declare (ignorable __function__))
    (and (symbolp x)
         (theorem-symbolp x wrld))))

Theorem: booleanp-of-theorem-namep

(defthm booleanp-of-theorem-namep
  (b* ((yes/no (theorem-namep x wrld)))
    (booleanp yes/no))
  :rule-classes :rewrite)