Major Section: MISCELLANEOUS
Example and General Form: ACL2 !>:redef! ACL2 p!>This command sets
ld-redefinition-action
to '(:warn! . :overwrite)
sets the default defun-mode to :
program
, and invokes
(set-state-ok t)
. It also introduces (defttag :redef!)
, so that
redefinition of system functions will be permitted; see defttag. Finally,
it removes as untouchable all variables and functions.
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!