Recognizer for a true list of integers
The predicate integer-listp tests whether its argument is a true list of integers.
Function: integer-listp
(defun integer-listp (l) (declare (xargs :guard t)) (cond ((atom l) (eq l nil)) (t (and (integerp (car l)) (integer-listp (cdr l))))))