|
|
|---|
|
|
|
|---|
Pre-translation step performed by ATJ: removal of all the trivial lambda-bound variables.
This is done only in the shallow embedding.
We remove all the lambda-bound variables, and corresponding actual arguments, that are identical to the corresponding actual arguments. See the discussion in remove-trivial-vars, which is the utility that we use to accomplish this pre-translation step.
This pre-translation step makes terms simpler to work with (for the purpose of ATJ) by only keeping the ``true'' lets in a term (which are lambda expressions in translated terms), avoiding the ``artificial'' ones to close the lambda expressions. Indeed, let terms are generally not closed in other languages, or even in ACL2's untranslated terms.