ACL2 Conses or Ordered Pairs

The function `cons` `Car` `cdr` `consp`

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

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