Major Section: ACL2-BUILT-INS
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=Yo Transitivity:
XrY & YrZ -> XrZo 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.
To see the ACL2 definition of this function, see pf.
