Defattach-system
Attach to built-in, system-level, constrained functions
For background on attachments, see defattach. The macro
defattach-system is a convenient way to attach to built-in functions.
The event (defattach f g) will fail if f is built into ACL2. This
failure can be overcome by specifying top-level keyword argument :system-ok
t, for example: (defattach (f g) :system-ok t). However, rather than
supplying this argument directly, it is recommended to use
defattach-system, which has the same syntax as defattach with two
exceptions: it adds :system-ok t automatically, that is, :system-ok
is implicit; and it expands to a local call of defattach. The
latter is important so that the attachment does not affect system behavior
outside a book containing the defattach event. Of course, if it is truly
intended to affect such behavior, the argument :system-ok t may be given
directly to defattach, without a surrounding use of local.
See system-attachments for discussion of system attachments. Also
see efficiency for how to use attachments to modify the prover's
behavior.
