Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Type-prescription
Rewrite
Meta
Force
Syntaxp
Extended-metafunctions
Meta-extract
Backchain-limit
Magic-ev-fncall
Evaluator-restrictions
Meta-implicit-hypothesis
Transparent-functions
Set-skip-meta-termp-checks
Case-split
Term-table
Magic-ev
Magic-ev-lst
Meta-lemmas
Set-skip-meta-termp-checks!
Linear
Definition
Clause-processor
Tau-system
Forward-chaining
Equivalence
Congruence
Free-variables
Executable-counterpart
Induction
Type-reasoning
Compound-recognizer
Rewrite-quoted-constant
Elim
Well-founded-relation-rule
Built-in-clause
Well-formedness-guarantee
Patterned-congruence
Rule-classes-introduction
Guard-holders
Refinement
Type-set-inverter
Generalize
Corollary
Induction-heuristics
Backchaining
Default-backchain-limit
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Magic-ev
Magic-ev-lst
Evaluate a list of terms using
magic-ev
.