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
atoms; the notion of ``non-strict total order'' is defined there.
Lexorder has a guard of
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.
compares two atoms by using
To see the ACL2 definition of this function, see pf.