		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

Atj-chars-to-jchars-id

Lift atj-char-to-jchars-id to lists.

Signature
(atj-chars-to-jchars-id chars startp uscore flip-case-p) → jchars
Arguments: chars — Guard (character-listp chars).; startp — Guard (booleanp startp).; uscore — Guard (member-eq uscore '(nil :dash :space)).; flip-case-p — Guard (booleanp flip-case-p).
Returns: jchars — Type (character-listp jchars), given (character-listp chars).

This is used on the sequence of characters that form an ACL2 symbol name or package name. The startp flag becomes nil at the first recursive call, because after the first character we are no longer at the start of the Java identifier.

Definitions and Theorems

Function: atj-chars-to-jchars-id

(defun atj-chars-to-jchars-id (chars startp uscore flip-case-p)
 (declare (xargs :guard (and (character-listp chars)
                             (booleanp startp)
                             (member-eq uscore '(nil :dash :space))
                             (booleanp flip-case-p))))
 (let ((__function__ 'atj-chars-to-jchars-id))
  (declare (ignorable __function__))
  (cond
     ((endp chars) nil)
     (t (append (atj-char-to-jchars-id (car chars)
                                       startp uscore flip-case-p)
                (atj-chars-to-jchars-id (cdr chars)
                                        nil uscore flip-case-p))))))

Theorem: character-listp-of-atj-chars-to-jchars-id

(defthm character-listp-of-atj-chars-to-jchars-id
 (implies
   (character-listp chars)
   (b*
    ((jchars
          (atj-chars-to-jchars-id chars startp uscore flip-case-p)))
    (character-listp jchars)))
 :rule-classes :rewrite)