defun.
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))
body))
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.