EQ

Major Section:  PROGRAMMING

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.