		Search-engine friendly clone of the ACL2 documentation.

Symbol<

Less-than test for symbols

(symbol< x y) is non-nil if and only if either the symbol-name of the symbol x lexicographically 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.

Function: symbol<

(defun symbol< (x y)
       (declare (xargs :guard (and (symbolp x) (symbolp y))))
       (let ((x1 (symbol-name x))
             (y1 (symbol-name y)))
            (or (string< x1 y1)
                (and (equal x1 y1)
                     (string< (symbol-package-name x)
                              (symbol-package-name y))))))