Recognize symbols that name functions introduced via defun-sk.
(defun-sk-namep x wrld) → yes/no
This function is enabled because it is meant as an abbreviation. Thus, theorems triggered by this function should be avoided.
(defun defun-sk-namep (x wrld) (declare (xargs :guard (plist-worldp wrld))) (let ((__function__ 'defun-sk-namep)) (declare (ignorable __function__)) (and (function-namep x wrld) (defun-sk-p x wrld) t)))
(defthm booleanp-of-defun-sk-namep (b* ((yes/no (defun-sk-namep x wrld))) (booleanp yes/no)) :rule-classes :rewrite)