Enhanced variant of primitivep.
This returns the same result as primitivep, but it causes an error if called on a symbol that does not name a function. This check requires an extra world argument (compared to primitivep), which is usually available when doing system programming.
(defun primitivep+ (fn wrld) (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld)))) (let ((__function__ 'primitivep+)) (declare (ignorable __function__)) (if (not (function-symbolp fn wrld)) (raise "The symbol ~x0 does not name a function." fn) (primitivep fn))))
(defthm booleanp-of-primitivep+ (b* ((yes/no (primitivep+ fn wrld))) (booleanp yes/no)) :rule-classes :rewrite)