		Search-engine friendly clone of the ACL2 documentation.

Defun-mode

Program

To set the default defun-mode to :program

Example:
ACL2 !>:program
ACL2 p!>

Typing the keyword :program sets the default defun-mode to :program.

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 mode.

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 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.

Subtopics

Program-wrapper: Avoiding expensive guard checks using program-mode functions