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