Major Section: ACL2-BUILT-INS
Eq 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
equal in the ACL2 logic.
Eq is a Common Lisp function. In order to ensure conformance
with Common Lisp, the ACL2 guard on eq requires at least one of
the arguments to eq to be a symbol. Common Lisp guarantees that
if x is a symbol, then x is eq to y if and only if x
is equal to y. Thus, the ACL2 user should think of eq as
nothing besides a fast means for checking equal when one argument
is known to be a symbol. In particular, it is possible that an
eq test will not even require the cost of a function call but
will be as fast as a single machine instruction.
