|
|
|---|
|
|
|
|---|
Pre-translation step performed by ATJ: renaming of the ACL2 variables.
This is done only in the shallow embedding.
We systematically rename all the ACL2 variables so that their new names are valid Java variable names and so that different ACL2 variables with the same name are renamed apart, unless the variables have been marked for reuse by the previous pre-translation step. This simplifies the ACL2-to-Java translation, which can just turn each ACL2 variable into a Java variable with the same name.