		Search-engine friendly clone of the ACL2 documentation.

Std/system/event-name-queries

Macro-namep

Recognize symbols that name macros.

Signature
(macro-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: macro-namep

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

Theorem: booleanp-of-macro-namep

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