|
|
|---|
|
|
|
|---|
Disallowed Java method names.
In the shallow embedding approach, ACL2 function names are turned into Java method names that must be valid identifiers. The mapping in atj-fn-to-method always produces characters that are valid for identifiers, but the sequence of such characters must not be a Java keyword, boolean or null literal, or empty.
This constant collects these disallowed names.
Definition:
(defconst *atj-disallowed-method-names* (append *jkeywords* *boolean-literals* (list *null-literal*) (list "")))