Atj-pre-translation-conjunctions
Pre-translation step performed by ATJ:
replacement of (if a b nil) calls with and calls.
This is done in the shallow embedding.
ACL2 turns untranslated calls of the form (and a b)
into translated calls of the form (if a b nil).
This pre-translation step performs the inverse transformation,
so that the ACL2-to-Java translation step can
more readily recognize this kind of calls
and treat them specially.
Note that this pre-translation step
turns (if a b nil) into (and a b)
even when the original untranslated term was (if a b nil).
But this is harmelss, as the two untranslated terms are equivalent.
Subtopics
- Atj-restore-and-calls-in-term
- Restore and calls in a translated term.
