Major Section: MISCELLANEOUS
Example and General Forms: (redefined-names state)
This function collects names that have been redefined in the current ACL2
state. :Program mode functions that were reclassified to
:logic functions are not collected, since such reclassification
cannot imperil soundness because it is allowed only when the new and old
definitions are identical.
Thus, if (redefined-names state) returns nil then no unsafe
definitions have been made, regardless of ld-redefinition-action.
See ld-redefinition-action.
WARNING: This function does not report names that are not explicitly redefined in the current logical world. Consider for example:
(encapsulate () (defun foo () t) (local (defun foo () nil)) (defthm foo-prop (equal (foo) nil) :rule-classes nil))If you attempt to call
certify-book in the resulting world, ACL2 will
appropriately refuse to do the certification:
ACL2 Error in (CERTIFY-BOOK "foo" ...): At least one command in the current ACL2 world was executed while the value of state global variable 'LD-REDEFINITION-ACTION was not nil: (DEFUN FOO NIL T) Certification is therefore not allowed in this world. You can use :ubt to undo back through this command; see :DOC ubt.However, since the local redefinition of
foo is gone in the certification
world, (redefined-names state) will return nil. (Technical aside,
to be ignored except for those interested in implementation details: ACL2
inhibits certify-book in this example because the definition of foo
is the value of (global-val 'redef-seen (w state)).)
