To set the default defun-mode to :program
Typing the keyword :program sets the default defun-mode to
Functions defined in :program mode are logically undefined but can be
executed on constants outside of deductive contexts. See defun-mode.
Calls of the following macros are ignored (skipped) when in :program
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 encapsulate events in
which it occurs. See ACL2-defaults-table.
Recall that the top-level form :program is equivalent to
(program); see keyword-commands. Thus, to change the default
defun-mode to :program in a book, use (program), which is an
embedded event form, rather than :program, which is not a legal form for
books. See embedded-event-form.
See program-wrapper for how to use program-mode functions to avoid
expensive guard checks.
- Avoiding expensive guard checks using program-mode functions