Search-engine friendly clone of the
ACL2 documentation
.
Top
Documentation
Books
Boolean-reasoning
Projects
Debugging
Std
Proof-automation
Macro-libraries
ACL2
Theories
Rule-classes
Proof-builder
Recursion-and-induction
Hons-and-memoization
Events
Parallelism
History
Programming
Defun
Declare
System-utilities
Stobj
State
Mutual-recursion
Memoize
Mbe
Io
Defpkg
Apply$
Loop$
Programming-with-state
Arrays
Characters
Time$
Loop$-primer
Fast-alists
Defconst
Defmacro
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
Oracle-eval
Defmacro-untouchable
Primitive
<<
Revert-world
Unmemoize
Set-duplicate-keys-action
Symbols
Def-list-constructor
Easy-simplify-term
Defiteration
Fake-oracle-eval
Defopen
Sleep
Operational-semantics
Real
Start-here
Debugging
Miscellaneous
Output-controls
Macros
Interfacing-tools
Interfacing-tools
Hardware-verification
Software-verification
Math
Testing-utilities
Programming
Conses
A
cons
is an ordered pair. In ACL2, data structures like
lists
,
alists
, etc., are made up of conses.
Subtopics
Cdr
Returns the second element of a
cons
pair, else
nil
Car
Returns the first element of a non-empty list, else
nil
Cons
Pair and list constructor
Consp
Recognizer for
cons
pairs
Cons-with-hint
Alternative to
cons
that tries to avoid consing when a suitable
cons
structure is provided as a hint.
Atom
Recognizer for atoms
Subst
A single substitution into a tree
Cadr
car
of the
cdr
Listp
Recognizer for (not necessarily proper) lists
Cons-count-bounded
Count the number of conses (up to a limit)
Cddr
cdr
of the
cdr
Caar
car
of the
car
Caddr
car
of the
cddr
Cdddr
cdr
of the
cddr
Cddar
cdr
of the
cdar
Cdar
cdr
of the
car
Cdadr
cdr
of the
cadr
Cdaar
cdr
of the
caar
Cadar
car
of the
cdar
Caadr
car
of the
cadr
Caaar
car
of the
caar
Cadddr
car
of the
cdddr
Caddar
car
of the
cddar
Cddddr
cdr
of the
cdddr
Cdddar
cdr
of the
cddar
Cddadr
cdr
of the
cdadr
Cddaar
cdr
of the
cdaar
Cdaddr
cdr
of the
caddr
Cdadar
cdr
of the
cadar
Cdaadr
cdr
of the
caadr
Cdaaar
cdr
of the
caaar
Cadadr
car
of the
cdadr
Cadaar
car
of the
cdaar
Caaddr
car
of the
caddr
Caadar
car
of the
cadar
Caaadr
car
of the
caadr
Caaaar
car
of the
caaar
