		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

atj-disallowed-jvar-names

Disallowed Java variable names.

The function atj-var-to-jvar turns an ACL2 symbol into one whose characters are all allowed in Java variables, but this is not sufficient: a Java variable name cannot be a keyword, a boolean literal, or the null literal.

This constant collects these disallowed sequences of characters, which otherwise consist of valid Java identifier characters. It also includes the empty sequence, because an ACL2 symbol may consist of no characters, but a Java identifier cannot be empty. It also includes the uppercase names of the t and nil symbols, because those are generated as static final fields, which would therefore conflict with homonymous variables.

Definition: *atj-disallowed-jvar-names*

(defconst *atj-disallowed-jvar-names*
  (append *jkeywords*
          *boolean-literals* (list *null-literal*)
          (list "")
          (list "T" "NIL")))