		Search-engine friendly clone of the ACL2 documentation.

Keywords

contextual-keywords

The contextual Java keywords, as ACL2 strings.

Definition: *contextual-keywords*

(defconst *contextual-keywords*
  (list "exports" "module" "non-sealed" "open"
        "opens" "permits" "provides" "record"
        "requires" "sealed" "to" "transitive"
        "uses" "var" "when" "with" "yield"))

Definitions and Theorems

Theorem: ascii-listp-of-*contextual-keywords*

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