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