Check if a list of ACL2 strings includes only ASCII Java identifiers.
(atj-string-ascii-java-identifier-listp x) → std::bool
This is an ordinary std::deflist. It is
"strict" in that it requires
Function:
(defun atj-string-ascii-java-identifier-listp (x) (declare (xargs :guard (string-listp x))) (let ((__function__ 'atj-string-ascii-java-identifier-listp)) (declare (ignorable __function__)) (if (consp x) (and (atj-string-ascii-java-identifier-p (car x)) (atj-string-ascii-java-identifier-listp (cdr x))) (null x))))