SYMBOL-<

less-than test for symbols
Major Section:  ACL2-BUILT-INS

(symbol-< x y) is non-nil if and only if either the symbol-name of the symbol x lexicographially precedes the symbol-name of the symbol y (in the sense of string<) or else the symbol-names are equal and the symbol-package-name of x lexicographically precedes that of y (in the same sense). So for example, (symbol-< 'abcd 'abce) and (symbol-< 'acl2::abcd 'foo::abce) are true.

The guard for symbol specifies that its arguments are symbols.

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