LEXORDER

Major Section:  PROGRAMMING

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.