the guard for the function eql
Major Section:  ACL2-BUILT-INS

The predicate eqlablep tests whether its argument is suitable for eql, at least one of whose arguments must satisfy this predicate in Common Lisp. (Eqlablep x) is true if and only if its argument is a number, a symbol, or a character.

To see the ACL2 definition of this function, see pf.