Total order on atoms
Also see lexorder, which extends
Within a single type: rationals are compared arithmetically, complex rationals are compared lexicographically, characters are compared via their char-codes, and strings and symbols are compared with alphabetic ordering. Across types, rationals come before complexes, complexes come before characters, characters before strings, and strings before symbols. We also allow for ``bad atoms,'' i.e., atoms that are not legal Lisp objects but make sense in the ACL2 logic; these come at the end, after symbols.
(defun alphorder (x y) (declare (xargs :guard (and (atom x) (atom y)))) (cond ((real/rationalp x) (cond ((real/rationalp y) (<= x y)) (t t))) ((real/rationalp y) nil) ((complex/complex-rationalp x) (cond ((complex/complex-rationalp y) (or (< (realpart x) (realpart y)) (and (= (realpart x) (realpart y)) (<= (imagpart x) (imagpart y))))) (t t))) ((complex/complex-rationalp y) nil) ((characterp x) (cond ((characterp y) (<= (char-code x) (char-code y))) (t t))) ((characterp y) nil) ((stringp x) (cond ((stringp y) (and (string<= x y) t)) (t t))) ((stringp y) nil) (t (cond ((symbolp x) (cond ((symbolp y) (not (symbol< y x))) (t t))) ((symbolp y) nil) (t (bad-atom<= x y))))))