System-level algorithms that users can modify with attachments
For background on attachments, see defattach.
If you evaluate the form
(ASSUME-TRUE-FALSE-AGGRESSIVE-P . CONSTANT-NIL-FUNCTION-ARITY-0)
We do not attempt to explain how to define functions to attach to system functions. We do however point out these two useful functions, for attaching to some constant functions (functions with arity 0).
To see how to use one of these functions, consider again the example above,
where constrained system function
(defattach-system assume-true-false-aggressive-p constant-t-function-arity-0)
Note that we are not explaining here what it means to make that algorithm more aggressive! We expect those who want to use these attachments to be comfortable as ``system programmers'', as they peruse the ACL2 source code and its comments in order to see how to modify system behavior with attachments. Perhaps more user-level documentation will be written to help with that process.
Also see efficiency for more about using attachments to modify the prover's behavior.