## 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.