• 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
        • Wormhole
        • Ld-skip-proofsp
        • Ld-redefinition-action
        • Lp
        • Ld-error-action
        • Ld-history
        • Guarantees-of-the-top-level-loop
        • Ld-post-eval-print
        • Ld-keyword-aliases
        • Current-package
        • Ld-query-control-alist
        • Ld-prompt
        • Keyword-commands
        • Redef+
        • Rebuild
        • Prompt
        • Ld-pre-eval-print
        • Calling-ld-in-bad-contexts
        • P!
        • Ld-pre-eval-filter
        • Ld-error-triples
        • Ld-evisc-tuple
        • Ld-verbose
        • A!
        • Default-print-prompt
        • Reset-ld-specials
        • Ld-always-skip-top-level-locals
        • Ld-missing-input-ok
        • Redef
        • Redef!
        • Redef-
        • I-am-here
        • Abort!
      • 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

• Ld

Redef

A common way to set ld-redefinition-action

Example and General Form:
ACL2 !>:redef

This command sets ld-redefinition-action to '(:query . :overwrite).

This command allows redefinition of functions and other events without undoing, but with a query that requires the user to acknowledge that the redefinition is intentional. To avoid that query, see redef!. For more options and an important warning about the danger of using redefinition, including possible unsoundness, see ld-redefinition-action.