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.