Java input types generated by ATJ.
ATJ generates certain Java types from corresponding ACL2 types; these Java types are used for methods' inputs (i.e. parameters).
ATJ also generates Java types for mv values, but those are only used for methods' outputs (i.e. results). We only consider input types here.
The Java code generated by ATJ also uses Java types other than the ones mentioned above, but those additional Java types are ``auxiliary'', in the sense that they are not the result of translating ACL2 types. We do not consider these auxiliary types here.