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
|
<html>
<head><title>ADD-BINOP.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>ADD-BINOP</h2>associate a binary function name with a macro name
<pre>Major Section: <a href="EVENTS.html">EVENTS</a>
</pre><p>
<pre>
Example:
(add-binop append binary-append)
</pre>
This example associates the function symbol <code><a href="BINARY-APPEND.html">binary-append</a></code> with the
macro name <code><a href="APPEND.html">append</a></code>. As a result, theory functions will understand
that <code>append</code> refers to <code>binary-append</code> -- see <a href="ADD-MACRO-ALIAS.html">add-macro-alias</a> --
and moreover, proof output will be printed using <code>append</code> rather than
<code>binary-append</code>, e.g., <code>(append x y z w)</code> is printed rather than
<code>(binary-append x (binary-append y (binary-append z w)))</code>.
<p>
<pre>
General Form:
(add-binop macro-name function-name)
</pre>
This is a convenient way to add an entry to <code><a href="MACRO-ALIASES-TABLE.html">macro-aliases-table</a></code>
and at the same time extend the <code>:</code><code><a href="BINOP-TABLE.html">binop-table</a></code>.
See <a href="MACRO-ALIASES-TABLE.html">macro-aliases-table</a>, see <a href="REMOVE-MACRO-ALIAS.html">remove-macro-alias</a>,
see <a href="BINOP-TABLE.html">binop-table</a>, and see <a href="REMOVE-BINOP.html">remove-binop</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>
|
