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