		Search-engine friendly clone of the ACL2 documentation.

Defun-mode

Logic

To set the default defun-mode to :logic

Example:
ACL2 p!>:logic
ACL2 !>

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

Functions defined in :logic mode are logically defined. See defun-mode.

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 :logic), and hence is local to any books and encapsulate events in which it occurs. See ACL2-defaults-table.

Recall that the top-level form :logic is equivalent to (logic); see keyword-commands. Thus, to change the default defun-mode to :logic in a book, use (logic), which is an embedded event form, rather than :logic, which is not a legal form for books. See embedded-event-form.