cons 
creates an ordered pair. Car
and cdr return the first and second components,
respectively, of an ordered pair. The function consp
recognizes ordered pairs.
The function cons creates an ordered pair. Car
and cdr return the first and second components,
respectively, of an ordered pair. The function consp
recognizes ordered pairs.
Ordered pairs are used to represent lists and trees. See any Common Lisp
documentation for a discussion of how list constants are written and for
the many list processing functions available. Also, see programming
where we list all the ACL2 primitive functions.
Here are some examples of list constants to suggest their syntax.
'(a . b) ; a pair whose car is 'a and cdr is 'b
'(a . nil) ; a pair whose car is 'a and cdr is nil
'(a) ; another way to write the same thing
'(a b) ; a pair whose car is 'a and cdr is '(b)
'(a b c) ; a pair whose car is 'a and cdr is '(b c)
; i.e., a list of three symbols, a, b, and c.
'((a . 1) (b . 2)) ; a list of two pairs
It is useful to distinguish ``proper'' conses from ``improper'' ones,
the former being those cons trees whose right-most branch terminates with
nil. A ``true list'' (see true-listp ) is either nil
or a proper cons. (A b c . 7) is an improper cons and hence not a
true list.
