		Search-engine friendly clone of the ACL2 documentation.

Hacker

Functions for extending ACL2 in ways that are potentially unsound.

The books/hacking library.

These functions typically require an active ttag (See defttag) to work.

In-raw-mode: Embed some raw lisp code as an event.
Progn+subsume-ttags: Execute some events, subsuming the specified ttags with the current ttag.
Ensure-program-only: Ensure that named functions are and remain in :PROGRAM mode.
Progn+touchable: Execute some events with some additional fns and/or vars made temporarily touchable.
Ensure-special-raw-definition-flag: Ensure that named functions are flagged as having special raw definitions.
Progn=touchable: Execute some events with only the specified fns and/or vars temporarily touchable.
Progn+redef: Execute some events but with redefinition enabled.
Ensure-program-only-flag: Ensure that given function names remain in :PROGRAM mode.
Defun-bridge: Define a function with a different low-level definition.
Assert-program-mode: Assert that given symbols name :PROGRAM mode functions.
Assert-no-special-raw-definition: Assert that given symbols do not have a special raw function definition.
With-redef-allowed: Execute some events but with redefinition enabled.
With-raw-mode: Embed some raw lisp code as an event.
With-touchable: Execute some events but with certain untouchables removed.