REDEF+

system hacker's redefinition command
Major Section:  MISCELLANEOUS

Example and General Form:
ACL2 !>:redef+
ACL2 p!>

This command is intended only for system hackers, not typical users. It sets ld-redefinition-action to '(:warn! . :overwrite), sets the default defun-mode to :program, and invokes set-state-ok with value t. It also introduces (defttag :redef+), so that redefinition of system functions will be permitted; see defttag. Finally, it removes as untouchable (see push-untouchable) all variables and functions.

WARNING: If the form (redef+) is used in a book, then including the book can leave you in a state in which dangerous actions are allowed, specifically: redefinition, and access to functions and variables normally prohibited because they are untouchable. To avoid this problem, insert the form (redef-) into your book after (redef+).

To see the code for redef+, evaluate :trans1 (redef+). This command is intended for those who are modifying ACL2 source code definitions. Thus, note that even system functions can be redefined with a mere warning. Be careful!