1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
|
<html>
<head><title>ACL2_Conses_or_Ordered_Pairs.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2 Conses or Ordered Pairs</h2>
<p>
The function <code><a href="CONS.html">cons</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> creates an ordered pair. <code><a href="CAR.html">Car</a></code>
<a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> and <code><a href="CDR.html">cdr</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a> return the first and second components,
respectively, of an ordered pair. The function <code><a href="CONSP.html">consp</a></code> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>
recognizes ordered pairs.<p>
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 <a href="PROGRAMMING.html">programming</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>
where we list all the ACL2 primitive functions.<p>
Here are some examples of list constants to suggest their syntax.
<pre>
'(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
</pre>
<p>
It is useful to distinguish ``proper'' conses from ``improper'' ones,
the former being those cons trees whose right-most branch terminates with
<code>nil</code>. A ``true list'' (see <a href="TRUE-LISTP.html">true-listp</a> <a href="A_Tiny_Warning_Sign.html"><img src=twarning.gif></a>) is either <code>nil</code>
or a proper cons. <code>(A b c . 7)</code> is an improper cons and hence not a
true list.
<br><br><br><a href="acl2-doc.html"><img src="llogo.gif"></a> <a href="acl2-doc-index.html"><img src="index.gif"></a>
</body>
</html>
|
