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
|
<html>
<head><title>MAXIMUM-LENGTH.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>MAXIMUM-LENGTH</h3>return the <code>:maximum-length</code> from the <a href="HEADER.html">header</a> of an array
<pre>Major Section: <a href="ARRAYS.html">ARRAYS</a>
</pre><p>
<pre>
Example Form:
(maximum-length 'delta1 a)
<p>
General Form:
(maximum-length name alist)
</pre>
where <code>name</code> is an arbitrary object and <code>alist</code> is a 1- or
2-dimensional array. This function returns the contents of the
<code>:maximum-length</code> field of the <a href="HEADER.html">header</a> of <code>alist</code>. Whenever an <code><a href="ASET1.html">aset1</a></code> or
<code><a href="ASET2.html">aset2</a></code> would cause the length of the alist to exceed its maximum
length, a <code><a href="COMPRESS1.html">compress1</a></code> or <code><a href="COMPRESS2.html">compress2</a></code> is done automatically to remove
irrelevant pairs from the array. <code>Maximum-length</code> operates in
virtually constant time if <code>alist</code> is the semantic value of <code>name</code>.
See <a href="ARRAYS.html">arrays</a>.
<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>
|
