Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
B*
Defunc
Fty
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
Std/util
Defdata
Defrstobj
Seq
Match-tree
Defrstobj
With-supporters
Def-partial-measure
Template-subst
Soft
Defthm-domain
Event-macros
Def-universal-equiv
Def-saved-obligs
With-supporters-after
Definec
Sig
Outer-local
Data-structures
ACL2
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Utilities
Hints-specifier-utilities
Some utilities for
hints specifiers.