Recognize true lists of symbols that name macros.
(macro-name-listp x wrld) → yes/no
This function is enabled because it is meant as an abbreviation. Theorems triggered by this function should be generally avoided.
(defun macro-name-listp (x wrld) (declare (xargs :guard (plist-worldp wrld))) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'macro-name-listp)) (declare (ignorable __function__)) (and (symbol-listp x) (macro-symbol-listp x wrld))))
(defthm booleanp-of-macro-name-listp (b* ((yes/no (macro-name-listp x wrld))) (booleanp yes/no)) :rule-classes :rewrite)