Check if a named function has raw Lisp code.
The global variables
This function checks whether a function has raw Lisp code by checking whether it is listed in one of those global variables.
(defun rawp (fn state) (declare (xargs :stobjs (state))) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'rawp)) (declare (ignorable __function__)) (and (or (member-eq fn (@ logic-fns-with-raw-code)) (member-eq fn (@ program-fns-with-raw-code))) t)))
(defthm booleanp-of-rawp (b* ((yes/no (rawp fn state))) (booleanp yes/no)) :rule-classes :rewrite)