Major Section: SWITCHES-PARAMETERS-AND-MODES
Example: ACL2 !>:program ACL2 p!>Typing the keyword
:programsets the default defun-mode to
Functions defined in
:program mode are logically undefined but can
be executed on constants outside of deductive contexts.
Calls of the following macros are ignored (skipped) when in
local verify-guards verify-termination defaxiom defthm deftheory in-theory in-arithmetic-theory regenerate-tau-database theory-invariant defchoose
Note: This is an event! It does not print the usual event summary but nevertheless changes the ACL2 logical world and is so recorded.
See defun-mode for a discussion of the defun-modes available
and what their effects on the logic are.
See default-defun-mode for a discussion of how the default
defun-mode is used. This event is equivalent to
(table acl2-defaults-table :defun-mode :program),
and hence is
local to any books and
in which it occurs. See acl2-defaults-table.
Recall that the top-level form
:program is equivalent to
see keyword-commands. Thus, to change the default defun-mode
:program in a book, use
(program), which is an embedded event
form, rather than
:program, which is not a legal form for books.