Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Acre
Milawa
Smtlink
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Aleobft
Proof-checker-array
Soft
Farray
Rp-rewriter
Rp-ruleset
Add-meta-rule
Enable-meta-rules
Disable-meta-rules
Def-rp-rule
Rp-pr
Enable-exc-counterpart
Disable-exc-counterpart
Bump-rules
Bump-rule
Bump-down-rule
Bump-all-meta-rules
Enable-rules
Enable-preprocessor
Enable-postprocessor
Disable-rules
Disable-preprocessor
Disable-postprocessor
Disable-all-rules
Defthmrp
Rp-rewriter/meta-rules
Rp-utilities
Rp-rewriter-demo
Rp-rewriter/debugging
Rp-rewriter/applications
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Bigmem-asymmetric
Des
Ethereum
Bigmem
Sha-2
Yul
X86isa
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Builtins
Axe
Execloader
Solidity
Leo
Paco
Concurrent-programs
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Rp-ruleset
Disable-meta-rules
Disable meta rules with given meta function name list.
See
rp-ruleset
for description.