cons creates an ordered pair.
cdr return the first and second components, respectively,
of an ordered pair. The function
consp recognizes ordered
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
(A b c . 7) is an improper cons and hence not a true