		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Pure-raw-p

Check if a function has raw Lisp code and is pure, i.e. it has no side effects.

Signature
(pure-raw-p fn) → yes/no
Arguments: fn — Guard (symbolp fn).
Returns: yes/no — Type (booleanp yes/no).

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, and whose unnormalized-body property therefore accurately describes the behavior of the function (despite the function being implemented natively for efficiency).

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.

Definitions and Theorems

Function: pure-raw-p

(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)))

Theorem: booleanp-of-pure-raw-p

(defthm booleanp-of-pure-raw-p
        (b* ((yes/no (pure-raw-p fn)))
            (booleanp yes/no))
        :rule-classes :rewrite)