		Search-engine friendly clone of the ACL2 documentation.

Portable-ascii-identifiers

Paident-char-listp

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.

Signature
(paident-char-listp chs) → yes/no
Arguments: chs — Guard (character-listp chs).
Returns: yes/no — Type (booleanp yes/no).

Sequences of characters satisfying these conditions may be portable ASCII identifiers, provided they are distinct from keywords.

Definitions and Theorems

Function: paident-char-listp

(defun paident-char-listp (chs)
  (declare (xargs :guard (character-listp chs)))
  (b* ((chs (str::character-list-fix chs)))
    (and (consp chs)
         (str::letter/digit/uscore-charlist-p chs)
         (not (str::dec-digit-char-p (car chs))))))

Theorem: booleanp-of-paident-char-listp

(defthm booleanp-of-paident-char-listp
  (b* ((yes/no (paident-char-listp chs)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: paident-char-listp-of-make-character-list-chs

(defthm paident-char-listp-of-make-character-list-chs
  (equal (paident-char-listp (make-character-list chs))
         (paident-char-listp chs)))

Theorem: paident-char-listp-charlisteqv-congruence-on-chs

(defthm paident-char-listp-charlisteqv-congruence-on-chs
  (implies (str::charlisteqv chs chs-equiv)
           (equal (paident-char-listp chs)
                  (paident-char-listp chs-equiv)))
  :rule-classes :congruence)