ALPHORDER

total order on atoms 
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 returns t or nil and satisfies the following properties.

o Antisymmetry: XrY & YrX -> X=Y

o Transitivity: XrY & YrZ -> XrZ

o Trichotomy: XrY v YrX

Also see lexorder, which extends alphorder to 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.