## <

less-than
Major Section: PROGRAMMING

Completion Axiom:

(equal (< x y)
(if (and (rationalp x)
(rationalp y))
(< x y)
(let ((x1 (if (acl2-numberp x) x 0))
(y1 (if (acl2-numberp y) y 0)))
(or (< (realpart x1) (realpart y1))
(and (equal (realpart x1) (realpart y1))
(< (imagpart x1) (imagpart y1)))))))

Guard for `(< x y)`

:

(and (rationalp x) (rationalp y))

Notice that like all arithmetic functions, `<`

treats non-numeric
inputs as `0`

.
This function has the usual meaning on the rational numbers, but is
extended to the complex rational numbers using the lexicographic
order: first the real parts are compared, and if they are equal,
then the imaginary parts are compared.