Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Hons-and-memoization
Events
History
Parallelism
Programming
Defun
Declare
Stobj
State
Memoize
Mbe
Io
Apply$
System-utilities
Defpkg
Mutual-recursion
Arrays
Programming-with-state
Characters
Loop$
Time$
Defmacro
Defconst
Guard
Evaluation
Equality-variants
Fast-alists
Compilation
Hons
ACL2-built-ins
Advanced-features
Set-check-invariant-risk
Developers-guide
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Alists
Set-register-invariant-risk
Strings
Program-wrapper
Get-internal-time
Basics
Let
Mv-let
Return-last
Or
Mv
And
Flet
Booleanp
If
Not
Equal
Implies
Iff
Quote
Let*
Case-match
ACL2-count
Good-bye
Exit
Quit
Cond
Case
Null
Progn$
Identity
Xor
Packages
System-attachments
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Defopen
Sleep
Real
ACL2-tutorial
Debugging
Miscellaneous
Prover-output
Built-in-theorems
Macros
Interfacing-tools
About-ACL2
Interfacing-tools
Hardware-verification
Software-verification
Testing-utilities
Math
Good-bye
Exit
Quit entirely out of Lisp
Same as
good-bye
.