1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
<html>
<head><title>EQ.html -- ACL2 Version 3.1</title></head>
<body text=#000000 bgcolor="#FFFFFF">
<h2>EQ</h2>equality of symbols
<pre>Major Section: <a href="PROGRAMMING.html">PROGRAMMING</a>
</pre><p>
<code>Eq</code> is the function for determining whether two objects are
identical (i.e., have the exact same store address in the current
von Neumann implementation of Common Lisp). It is the same as
<code><a href="EQUAL.html">equal</a></code> in the ACL2 logic.
<p>
<code>Eq</code> is a Common Lisp function. In order to ensure conformance
with Common Lisp, the ACL2 <a href="GUARD.html">guard</a> on <code>eq</code> requires at least one of
the arguments to <code>eq</code> to be a symbol. Common Lisp guarantees that
if <code>x</code> is a symbol, then <code>x</code> is <code>eq</code> to <code>y</code> if and only if <code>x</code>
is <code><a href="EQUAL.html">equal</a></code> to <code>y</code>. Thus, the ACL2 user should think of <code>eq</code> as
nothing besides a fast means for checking <code><a href="EQUAL.html">equal</a></code> when one argument
is known to be a symbol. In particular, it is possible that an
<code>eq</code> test will not even require the cost of a function call but
will be as fast as a single machine instruction.
<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>
|
