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>_at_.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>@</h2>get the value of a global variable in <code><a href="STATE.html">state</a></code>
<pre>Major Section: <a href="OTHER.html">OTHER</a>
</pre><p>
<pre>
Examples:
(+ (@ y) 1)
(assign a (aset1 'ascii-map-array (@ a) 66 'Upper-case-B))
<p>
General Form:
(@ symbol)
</pre>
where <code>symbol</code> is any symbol to which you have <code><a href="ASSIGN.html">assign</a></code>ed a global
value. This macro expands into <code>(f-get-global 'symbol state)</code>, which
retrieves the stored value of the symbol.<p>
The macro <code><a href="ASSIGN.html">assign</a></code> makes it convenient to set the value of a symbol.
The <code>:</code><code><a href="UBT.html">ubt</a></code> operation has no effect on the <code>global-table</code> of <code><a href="STATE.html">state</a></code>.
Thus, you may use these globals to hang onto useful data structures
even though you may undo back past where you computed and saved
them.
<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>
|
