REDEFINED-NAMES

to collect the names that have been redefined
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.