ACL2 Conses or 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.