Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
X86isa
Program-execution
Introduction
X86isa-build-instructions
Publications
Contributors
Machine
Implemented-opcodes
Proof-utilities
To-do
Concrete-simulation-examples
Model-validation
Utils
Structures
Utilities
Constants-conversions-and-bounds
Globally-disabled-events
Mk-name
Debugging-code-proofs
Axe
Execloader
Testing-utilities
Math
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.