### LEXORDER

total order on ACL2 objects
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
`cdr`

s being compared only if the `car`

s are equal. `Lexorder`

compares two atoms by using `alphorder`

.

To see the ACL2 definition of this function, see pf.