Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Community
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Kestrel-books
Crypto-hdwallet
Apt
Error-checking
Fty-extensions
Isar
Kestrel-utilities
Set
C
Soft
Bv
Imp-language
Ethereum
Event-macros
Java
Riscv
Bitcoin
Zcash
Yul
ACL2-programming-language
Prime-fields
Json
Syntheto
File-io-light
Cryptography
Number-theory
Axe
Axe-r1cs
Axe-lifters
Axe-core
Prove-equal-with-axe
Dags
Stp
Rewriter-legacy
Rewriter-basic
Rewriter-alt
Prover-basic
Make-rewriter-simple
Make-prover-simple
Defthm-stp
Defthm-axe-basic
Def-simplified
Prover-legacy
Axe-provers
Axe-rewriters
Axe-jvm
Axe-x86
Axe-risc-v
Lists-light
Builtins
Solidity
Helpers
Htclient
Typed-lists-light
Arithmetic-light
X86isa
Axe
Axe-r1cs
Axe-lifters
Axe-core
Prove-equal-with-axe
Dags
Stp
Rewriter-legacy
Rewriter-basic
Rewriter-alt
Prover-basic
Make-rewriter-simple
Make-prover-simple
Defthm-stp
Defthm-axe-basic
Def-simplified
Prover-legacy
Axe-provers
Axe-rewriters
Axe-jvm
Axe-x86
Axe-risc-v
Execloader
Math
Testing-utilities
Axe
Axe-core
The core Axe tools.
Many of the core Axe tools are independent of which Axe variant is used.
Subtopics
Prove-equal-with-axe
A tool for proving that DAGs / terms are equivalent.
Dags
Axe's DAG data structure.
Stp
An SMT solver used by the Axe toolkit.
Rewriter-legacy
The legacy Axe rewriter.
Rewriter-basic
A basic, modern Axe rewriter.
Rewriter-alt
Another legacy Axe rewriter.
Prover-basic
A basic, modern Axe prover.
Make-rewriter-simple
A tool to create custom Axe rewriters.
Make-prover-simple
A tool to create custom Axe prover.
Defthm-stp
A defthm-like tool that uses the STP solver.
Defthm-axe-basic
A defthm-like tool that uses Axe.
Def-simplified
A tool to simplify a term or DAG.
Prover-legacy
The legacy Axe prover.
