Check if a named function is primitive.
See primitivep+ for an enhanced variant of this utility.
(defun primitivep (fn) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'primitivep)) (declare (ignorable __function__)) (and (member-eq fn (strip-cars *primitive-formals-and-guards*)) t)))
(defthm booleanp-of-primitivep (b* ((yes/no (primitivep fn))) (booleanp yes/no)) :rule-classes :rewrite)
(defthm primitivep-forward-to-symbolp (implies (primitivep fn) (symbolp fn)) :rule-classes :forward-chaining)