• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
  • Proof-automation
  • Macro-libraries
  • ACL2
    • Theories
    • Rule-classes
    • Proof-builder
    • Recursion-and-induction
    • Hons-and-memoization
    • Events
    • Parallelism
    • History
    • Programming
    • Operational-semantics
    • Real
    • Start-here
    • Debugging
    • Miscellaneous
      • Term
      • Ld
      • Hints
      • Type-set
      • Ordinals
      • Clause
      • ACL2-customization
      • With-prover-step-limit
      • Set-prover-step-limit
      • With-prover-time-limit
      • Local-incompatibility
      • Set-case-split-limitations
      • Subversive-recursions
      • Specious-simplification
      • Defsum
      • Gcl
      • Oracle-timelimit
      • Thm
      • Defopener
      • Case-split-limitations
      • Set-gc-strategy
      • Default-defun-mode
      • Top-level
      • Reader
      • Ttags-seen
      • Adviser
      • Ttree
      • Abort-soft
      • Defsums
      • Gc$
      • With-timeout
      • Coi-debug::fail
      • Expander
      • Gc-strategy
      • Coi-debug::assert
      • Sin-cos
      • Def::doc
      • Syntax
      • Subversive-inductions
    • Output-controls
    • Macros
    • Interfacing-tools
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Miscellaneous

Default-defun-mode

The default defun-mode of defun'd functions

When a defun is processed and no :mode xarg is supplied, the function default-defun-mode is used. To find the default defun-mode of the current ACL2 world, type (default-defun-mode (w state)). See defun-mode for a discussion of defun-modes. To change the default defun-mode of the ACL2 world, type one of the keywords :program or :logic.

The default ACL2 prompt displays the current default defun-mode by showing the character p for :program mode, and omitting it for :logic mode; see default-print-prompt. The default defun-mode may be changed using the keyword commands :program and :logic, which are equivalent to the commands (program) and (logic). Each of these names is documented separately: see program and see logic. The default defun-mode is stored in the table ACL2-defaults-table and hence may also be changed by a table command. See table and also see ACL2-defaults-table. Both mode-changing commands are events.

While events that change the default defun-mode are permitted within an encapsulate or the text of a book, their effects are local in scope to the duration of the encapsulation or inclusion. For example, if the default defun-mode is :logic and a book is included that contains the event (program), then subsequent events within the book are processed with the default defun-mode :program; but when the include-book event completes, the default defun-mode will still be :logic. Commands that change the default defun-mode are not permitted inside local forms.