Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Apt
Simplify-defun
Isodata
Tailrec
Schemalg
Restrict
Expdata
Casesplit
Simplify-term
Simplify-defun-sk
Parteval
Solve
Wrap-output
Propagate-iso
Simplify
Finite-difference
Drop-irrelevant-params
Copy-function
Lift-iso
Rename-params
Utilities
Defaults-table
Xdoc::apt-constructors
Input-processors
Transformation-table
Find-base-cases
Untranslate-specifier-utilities
Print-specifier-utilities
Hints-specifier-utilities
Simplify-term-programmatic
Simplify-defun-sk-programmatic
Simplify-defun-programmatic
Simplify-defun+
Common-options
Common-concepts
Acre
Milawa
Smtlink
Aleobft
Abnf
Vwsim
Isar
Wp-gen
Dimacs-reader
Pfcs
Legacy-defrstobj
Proof-checker-array
Soft
Farray
Rp-rewriter
Instant-runoff-voting
Imp-language
Sidekick
Leftist-trees
C
Java
Taspi
Bitcoin
Des
Ethereum
X86isa
Sha-2
Yul
Riscv
Zcash
Proof-checker-itp13
Regex
ACL2-programming-language
Json
Jfkr
Equational
Cryptography
Poseidon
Where-do-i-place-my-book
Bigmems
Builtins
Axe
Execloader
Solidity
Leo
Paco
Concurrent-programs
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Apt
Utilities
Utilities shared by the implementations of the APT tools.
Subtopics
Defaults-table
APT defaults table.
Xdoc::apt-constructors
Utilities to construct
XDOC strings to document
APT transformations.
Input-processors
Utilities to process inputs that are common to multiple APT transformations.
Transformation-table
APT transformation table.
Find-base-cases
Utilities to find base cases of recursive function definitions.
Untranslate-specifier-utilities
Some utilities for
untranslate specifiers.
Print-specifier-utilities
Some utilities for
print specifiers.
Hints-specifier-utilities
Some utilities for
hints specifiers.