1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
<html>
<head><title>ACL2-COUNT.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ACL2-COUNT</h2>a commonly used measure for justifying recursion
<pre>Major Section: <a href="MISCELLANEOUS.html">MISCELLANEOUS</a>
</pre><p>
<code>(Acl2-count x)</code> returns a nonnegative integer that indicates the
``size'' of its argument <code>x</code>.
<p>
All <a href="CHARACTERS.html">characters</a> and symbols have <code>acl2-count 0</code>. The <code>acl2-count</code> of a
string is the number of <a href="CHARACTERS.html">characters</a> in it, i.e., its length. The
<code>acl2-count</code> of a <code><a href="CONS.html">cons</a></code> is one greater than the sum of the <code>acl2-count</code>s
of the <code><a href="CAR.html">car</a></code> and <code><a href="CDR.html">cdr</a></code>. The <code>acl2-count</code> of an integer is its absolute
value. The <code>acl2-count</code> of a rational is the sum of the <code>acl2-count</code>s
of the numerator and denominator. The <code>acl2-count</code> of a complex
rational is one greater than the sum of the <code>acl2-count</code>s of the real
and imaginary parts.
<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>
|
