Lexorder
Total order on ACL2 objects
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.
Function: lexorder
(defun lexorder (x y)
(declare (xargs :guard t))
(cond ((atom x)
(cond ((atom y) (alphorder x y)) (t t)))
((atom y) nil)
((equal (car x) (car y))
(lexorder (cdr x) (cdr y)))
(t (lexorder (car x) (car y)))))Subtopics
- Fast-lexorder
- Probably faster alternative to lexorder.
