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