		Search-engine friendly clone of the ACL2 documentation.

Keywords

jkeywords

The (non-restricted) Java keywords, as ACL2 strings.

Definition: *jkeywords*

(defconst *jkeywords*
  (list "abstract" "assert" "boolean" "break"
        "byte" "case" "catch" "char" "class"
        "const" "continue" "default" "do"
        "double" "else" "enum" "extends" "final"
        "finally" "float" "for" "if" "goto"
        "implements" "import" "instanceof"
        "int" "interface" "long" "native" "new"
        "package" "private" "protected" "public"
        "return" "short" "static" "strictfp"
        "super" "switch" "synchronized"
        "this" "throw" "throws" "transient"
        "try" "void" "volatile" "while" "_"))

Definitions and Theorems

Theorem: ascii-listp-of-*jkeywords*

(defthm ascii-listp-of-*jkeywords*
  (implies (member-equal keyword *jkeywords*)
           (ascii-listp (string=>unicode keyword))))