Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Recursion-and-induction
Boolean-reasoning
Debugging
Projects
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Hons-and-memoization
Events
History
Parallelism
Programming
Defun
Declare
System-utilities
Stobj
State
Memoize
Mbe
Io
Apply$
Defpkg
Mutual-recursion
Loop$
Programming-with-state
Arrays
Characters
Time$
Loop$-primer
Fast-alists
Defmacro
Defconst
Evaluation
Guard
Equality-variants
Compilation
Hons
ACL2-built-ins
Developers-guide
System-attachments
Advanced-features
Set-check-invariant-risk
Numbers
Irrelevant-formals
Efficiency
Introduction-to-programming-in-ACL2-for-those-who-know-lisp
Redefining-programs
Lists
Invariant-risk
Errors
Defabbrev
Conses
Cdr
Car
Cons
Consp
Cons-with-hint
Atom
Subst
Cadr
Listp
Cons-count-bounded
Cddr
Caar
Caddr
Cdddr
Cddar
Cdar
Cdadr
Cdaar
Cadar
Caadr
Caaar
Cadddr
Caddar
Cddddr
Cdddar
Cddadr
Cddaar
Cdaddr
Cdadar
Cdaadr
Cdaaar
Cadadr
Cadaar
Caaddr
Caadar
Caaadr
Caaaar
Alists
Set-register-invariant-risk
Strings
Program-wrapper
Get-internal-time
Basics
Packages
Defmacro-untouchable
Primitive
<<
Revert-world
Set-duplicate-keys-action
Unmemoize
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Defopen
Sleep
Start-here
Real
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Testing-utilities
Math
Conses
ACL2-built-ins
Caaadr
car
of the
caadr
See any Common Lisp documentation for details.