		Search-engine friendly clone of the ACL2 documentation.

World

Redefined-names

To collect the names that have been redefined

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)).)