the default ruler-extenders for defun'd functions

When a defun is processed and no :ruler-extenders xarg is supplied, the function default-ruler-extenders is used to obtain the current ruler-extenders; see ruler-extenders. To find the default ruler-extenders of the current ACL2 world, type (default-ruler-extenders (w state)).

While events that change the default ruler-extenders are permitted within an encapsulate or the text of a book, their effects are local in scope to the duration of the encapsulation or inclusion. See default-defun-mode for an analogous discussion for defun-modes.