		Search-engine friendly clone of the ACL2 documentation.

Integer-range-listp

Recognize true lists of integers in ranges.

Signature
(integer-range-listp lower upper x) → std::bool

This lifts integer-range-p to lists. The range goes from lower inclusive to upper exclusive, as in integer-range-p.

Definitions and Theorems

Function: integer-range-listp

(defun integer-range-listp (lower upper x)
       (declare (xargs :guard (and (integerp lower)
                                   (integerp upper))))
       (let ((__function__ 'integer-range-listp))
            (declare (ignorable __function__))
            (if (consp x)
                (and (integer-range-p lower upper (car x))
                     (integer-range-listp lower upper (cdr x)))
                (null x))))

Subtopics

Integer-range-listp-basics: Basic theorems about integer-range-listp, generated by std::deflist.
Integer-range-list-fix: Fixing function for integer-range-listp.