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
Testing-utilities
Math
Arithmetic
Lispfloat
Arithmetic-1
Number-theory
Proof-by-arith
Arith-equivs
Number-theory
Arithmetic-3
Arithmetic-2
Arithmetic-light
Arithmetic-5
Bit-vectors
Algebra
Arithmetic
Arithmetic-3
Another newer arithmetic library that is considered deprecated in favor of arithmetic-5.
For more information, see
arithmetic-3/README
.