		Search-engine friendly clone of the ACL2 documentation.

Std/system/function-queries

Non-executablep

Non-executable status of a named function.

Signature
(non-executablep fn wrld) → status
Arguments: fn — Guard (symbolp fn).; wrld — Guard (plist-worldp wrld).
Returns: status — t, nil, or :program.

See non-executablep+ for an enhanced variant of this utility.

Definitions and Theorems

Function: non-executablep

(defun non-executablep (fn wrld)
  (declare (xargs :guard (and (symbolp fn) (plist-worldp wrld))))
  (let ((__function__ 'non-executablep))
    (declare (ignorable __function__))
    (getpropc fn 'non-executablep
              nil wrld)))