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
Cdr
Car
Cons
Consp
Cons-with-hint
Atom
Subst
Listp
Cadr
Cons-count-bounded
Caar
Caddr
Cdddr
Cddr
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
Program-wrapper
Strings
Get-internal-time
Basics
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
Conses
ACL2-built-ins
Cdar
cdr
of the
car
See any Common Lisp documentation for details.