		Search-engine friendly clone of the ACL2 documentation.

Atj-name-translation

atj-predefined-method-names

Predefined Java method names for certain ACL2 functions.

Certain primitive ACL2 functions are generally used frequently, and thus we want to use more readable Java method names than would be produced by the default translation in atj-fn-to-method. In particular, the default translation for unary-- would be unary__, even though the second dash is not really a separator but rather stands for the `minus' sign: for this function, we want to use the more readable unary_minus method name. Other primitive functions like binary-+ would include $ escapes according to their default translation; while not as bad as the default for unary--, we want to use more readable method names like binary_plus.

We store these predefined method names as values of this alist, whose keys are the corresponding primitive functions. This alist is used in atj-fn-to-method.

These predefined names currently use lowercase letters separated by underscores, consistently with the character translation in atj-chars-to-jchars-id.

Definition: *atj-predefined-method-names*

(defconst *atj-predefined-method-names*
  '((bad-atom<= . "bad_atom_less_than_or_equal_to")
    (binary-* . "binary_star")
    (binary-+ . "binary_plus")
    (unary-- . "unary_minus")
    (unary-/ . "unary_slash")
    (< . "less_than")))