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