		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))))))