		Search-engine friendly clone of the ACL2 documentation.

Identifiers

Identifier-grammar-chars-p

Check if a list of characters forms a Leo identifier according to the ABNF grammar rule for identifiers.

Signature
(identifier-grammar-chars-p chars) → yes/no
Arguments: chars — Guard (character-listp chars).
Returns: yes/no — Type (booleanp yes/no).

The list must start with a letter and only contain letters, digits, and underscores. This is exactly what the grammar rule requires, but there are also extra-grammatical requirements, captured in identifier-string-p

Definitions and Theorems

Function: identifier-grammar-chars-p

(defun identifier-grammar-chars-p (chars)
  (declare (xargs :guard (character-listp chars)))
  (let ((__function__ 'identifier-grammar-chars-p))
    (declare (ignorable __function__))
    (b* ((chars (str::character-list-fix chars)))
      (and (consp chars)
           (str::letter-char-p (car chars))
           (str::letter/digit/uscore-charlist-p (cdr chars))))))

Theorem: booleanp-of-identifier-grammar-chars-p

(defthm booleanp-of-identifier-grammar-chars-p
  (b* ((yes/no (identifier-grammar-chars-p chars)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: identifier-grammar-chars-p-of-make-character-list-chars

(defthm identifier-grammar-chars-p-of-make-character-list-chars
  (equal (identifier-grammar-chars-p (make-character-list chars))
         (identifier-grammar-chars-p chars)))

Theorem: identifier-grammar-chars-p-charlisteqv-congruence-on-chars

(defthm identifier-grammar-chars-p-charlisteqv-congruence-on-chars
  (implies (str::charlisteqv chars chars-equiv)
           (equal (identifier-grammar-chars-p chars)
                  (identifier-grammar-chars-p chars-equiv)))
  :rule-classes :congruence)