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
|
<html>
<head><title>DIMENSIONS.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h3>DIMENSIONS</h3>return the <code>:dimensions</code> from the <a href="HEADER.html">header</a> of a 1- or 2-dimensional array
<pre>Major Section: <a href="ARRAYS.html">ARRAYS</a>
</pre><p>
<pre>
Example Form:
(dimensions 'delta1 a)
<p>
General Form:
(dimensions name alist)
</pre>
where <code>name</code> is arbitrary and <code>alist</code> is a 1- or 2-dimensional array.
This function returns the dimensions list of the array <code>alist</code>. That
list will either be of the form <code>(dim1)</code> or <code>(dim1 dim2)</code>, depending on
whether <code>alist</code> is a 1- or 2-dimensional array. <code>Dim1</code> and <code>dim2</code> will be
integers and each exceed by 1 the maximum legal corresponding index.
Thus, if <code>dimensions</code> returns, say, <code>'(100)</code> for an array <code>a</code>
named <code>'delta1</code>, then <code>(aref1 'delta1 a 99)</code> is legal but
<code>(aref1 'delta1 a 100)</code> violates the <a href="GUARD.html">guard</a>s on <code><a href="AREF1.html">aref1</a></code>.
<code>Dimensions</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>
|
