Major Section: PROGRAMMING
Alphorder is a non-strict total order, a ``less than or equal,'' on
atoms. By ``non-strict total order'' we mean a function that always
nil and satisfies the following properties.
Also see lexorder, which extends
XrY & YrX -> X=Y
XrY & YrZ -> XrZ
XrY v YrX
alphorderto all objects.
(Alphorder x y) has a guard of
(and (atom x) (atom y)).
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.