Check if a function has raw Lisp code and is pure, i.e. it has no side effects.
This utility checks whether the symbol is
in a whitelist of function symbols that have raw Lisp code
and that are known to be free of side effects,
The fact that a function with raw Lisp code is not in this whitelist does not necessarily mean that it has side effects. It just means that it is currently not known to be free of side effects. The whitelist may be extended as needed.
(defun pure-raw-p (fn) (declare (xargs :guard (symbolp fn))) (let ((__function__ 'pure-raw-p)) (declare (ignorable __function__)) (and (member-eq fn *pure-raw-p-whitelist*) t)))
(defthm booleanp-of-pure-raw-p (b* ((yes/no (pure-raw-p fn))) (booleanp yes/no)) :rule-classes :rewrite)