(letter/digit/uscore-charlist-p x) recognizes lists where every element satisfies letter/digit/uscore-char-p.
(letter/digit/uscore-charlist-p x) → std::bool
This is an ordinary std::deflist. It is
"loose" in that it does not care whether
Function:
(defun letter/digit/uscore-charlist-p (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'letter/digit/uscore-charlist-p)) (declare (ignorable acl2::__function__)) (if (consp x) (and (letter/digit/uscore-char-p (car x)) (letter/digit/uscore-charlist-p (cdr x))) t)))
Theorem:
(defthm chars-in-charset-p-of-letter/digit/uscore-chars (equal (chars-in-charset-p x (letter/digit/uscore-chars)) (letter/digit/uscore-charlist-p x)))