Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
X86isa
Program-execution
Sdm-instruction-set-summary
Tlb
Booting-linux
Introduction
Asmtest
X86isa-build-instructions
Publications
Contributors
Machine
Implemented-opcodes
To-do
Proof-utilities
Peripherals
Model-validation
Modelcalls
Concrete-simulation-examples
Utils
Structures
Utilities
Constants-conversions-and-bounds
Globally-disabled-events
Mk-name
Debugging-code-proofs
Axe
Execloader
Math
Testing-utilities
Utils
Utilities
Subtopics
Constants-conversions-and-bounds
Definitions of commonly used constants and some functions to convert between
natp
and
integerp
, etc.
Globally-disabled-events
A ruleset containing all the events supposed to be mostly globally disabled in our books
Mk-name
Macro that can be used to create event names by concatenating strings, symbols, numbers, and characters.