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
37
|
<html>
<head><title>NTH-ALIASES-TABLE.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>NTH-ALIASES-TABLE</h2>a <a href="TABLE.html">table</a> used to associate names for nth/update-nth printing
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(table nth-aliases-table 'st0 'st)
</pre>
This example associates the symbol <code>st0</code> with the symbol <code>st</code>. As a
result, when the theorem prover prints terms of the form
<code>(nth n st0)</code> or <code>(update-nth n val st0)</code>, where <code>st</code> is a <a href="STOBJ.html">stobj</a>
whose <code>n</code>th accessor function is <code>f-n</code>, then it will print <code>n</code> as
<code>*f-n*</code>.
<p>
<pre>
General Form:
(table nth-aliases-table 'alias-name 'name)
</pre>
This event causes <code>alias-name</code> to be treated like <code>name</code> for purposes
of the printing of terms that are calls of <code>nth</code> and <code>update-nth</code>.
(Note however that <code>name</code> is not recursively looked up in this
table.) Both must be symbols other than <code><a href="STATE.html">state</a></code>. See <a href="TERM.html">term</a>, in
particular the discussion there of untranslated terms.<p>
For a convenient way to add entries to this <a href="TABLE.html">table</a>,
see <a href="ADD-NTH-ALIAS.html">add-nth-alias</a>. To remove entries from the <a href="TABLE.html">table</a> with ease,
see <a href="REMOVE-NTH-ALIAS.html">remove-nth-alias</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>
|
