Check if a list of ACL2 characters is not empty, consists only of ASCII letters, digits, and underscores, and does not start with a digit.
(paident-char-listp chs) → yes/no
Sequences of characters satisfying these conditions may be portable ASCII identifiers, provided they are distinct from keywords.
Function:
(defun paident-char-listp (chs) (declare (xargs :guard (character-listp chs))) (let ((__function__ 'paident-char-listp)) (declare (ignorable __function__)) (and (consp chs) (str::letter/digit/uscore-charlist-p chs) (not (str::dec-digit-char-p (car chs))))))
Theorem:
(defthm booleanp-of-paident-char-listp (b* ((yes/no (paident-char-listp chs))) (booleanp yes/no)) :rule-classes :rewrite)