Major Section: ACL2-BUILT-INS
Lexorder is a non-strict total order, a ``less than or equal,'' on
ACL2 objects. Also see alphorder, the restriction of lexorder to
atoms; the notion of ``non-strict total order'' is defined there.
Lexorder has a guard of t.
For lexorder, an atom and a cons are ordered so that
the atom comes first, and two conses are ordered so that
the one with the recursively smaller car comes first, with the
cdrs being compared only if the cars are equal. Lexorder
compares two atoms by using alphorder.
To see the ACL2 definition of this function, see pf.
