(vl-maybe-nat-listp x) recognizes lists where every element satisfies maybe-natp.
(vl-maybe-nat-listp x) → std::bool
This is an ordinary deflist. It is
"loose" in that it does not care whether
(defun vl-maybe-nat-listp (x) (declare (xargs :guard t)) (let ((__function__ 'vl-maybe-nat-listp)) (declare (ignorable __function__)) (if (consp x) (and (maybe-natp (car x)) (vl-maybe-nat-listp (cdr x))) t)))
(defthm nat-listp-when-no-nils-in-vl-maybe-nat-listp (implies (and (not (member-equal nil x)) (vl-maybe-nat-listp x)) (nat-listp x)))