define a non-executable function symbol
Major Section:  EVENTS

The macro defun-nx introduces definitions using the defun macro, always in :logic mode, such that the calls of the resulting function cannot be evaluated. Such a definition is admitted without the syntactic restrictions usually imposed on definitions, as opposed to theorems, in particular regarding function signatures and the use of single-threaded object names, even though such functions are permitted to declare names to be :stobjs.

The syntax is identical to that of defun. A form

(defun-nx name (x1 ... xk) ... body)
expands to the following form.
(defun name (x1 ... xk)
  (declare (xargs :non-executable t :mode :logic))
  (prog2$ (throw-nonexec-error 'name (list x1 ... xk))
Note that because of the insertion of the above call of throw-nonexec-error, no formal is ignored when using defun-nx.

If you prefer to avoid the use of defun-nx for non-executable function definitions in :logic mode, you can use an xargs :non-executable t declare form, provided the body has the form (prog2$ (throw-nonexec-error ...) ...). The function throw-nonexec-error is guaranteed to cause an error, though the :non-executable keyword will lay down code such that an error generally occurs when calling name without calling throw-nonexec-error.

During proofs, the error is silent; it is ``caught'' by the proof mechanism and generally results in the introduction of a call of hide during a proof. If an error message is produced by evaluating a call of the function on a list of arguments that includes state or user-defined stobjs, these arguments will be shown as symbols such as |<state>| in the error message.

It is harmless to include :non-executable t in your own xargs declare form; defun-nx will still lay down its own such declaration, but ACL2 can tolerate the duplication.

See defun for documentation of defun.