Check if a named function has raw Lisp code.
(rawp fn state) → yes/no
- fn — Guard (symbolp fn).
- yes/no — Type (booleanp yes/no).
The global variables
logic-fns-with-raw-code and program-fns-with-raw-code
list the logic-mode and program-mode functions with raw Lisp code.
Their initial values are
but they may change if functions with raw Lisp code are introduced.
This function checks whether a function has raw Lisp code
by checking whether it is listed in one of those global variables.
Definitions and Theorems
(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)))
(b* ((yes/no (rawp fn state)))