Eq
Equality of symbols
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.
Function: eq
(defun eq (x y)
(declare (xargs :guard (if (symbolp x) t (symbolp y))))
(equal x y))
