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