Recognize lists of ATJ Java input types.
(atj-jitype-listp x) → std::bool
This is an ordinary std::deflist. It is
"strict" in that it requires
Function:
(defun atj-jitype-listp (x) (declare (xargs :guard t)) (let ((__function__ 'atj-jitype-listp)) (declare (ignorable __function__)) (if (consp x) (and (atj-jitypep (car x)) (atj-jitype-listp (cdr x))) (null x))))
Theorem:
(defthm jtype-listp-when-atj-jitype-listp (implies (atj-jitype-listp x) (jtype-listp x)))