A formalization of ACL2 translated terms.

ACL2 terms may be untranslated (i.e. user-facing) or translated (i.e. internal). Here we formalize translated terms, which we essentially regard as abstract syntax of the ACL2 programming language. We may also formalize untranslated terms at some point, but for now it seems that translated terms should suffice for an initial formalization of the ACL2 programming language.

We formalize translated terms as free algebraic structures,
without the world-related constraints
(e.g. that all function symbols are in the world),
and even without some of the constraints included in `pseudo-termp`
(e.g. that the number of actual arguments of a lambda call
matches the number of parameters of the lambda expression).
These well-formedness constraints may be formalized separately.

We use (free) fixtypes to formalize translated terms.
As noted above, these fixtypes are a bit larger than `pseudo-termp`.
Thus, the fixtypes introduced here differ slightly from the pseudo-term fixtypes, which are consistent with `pseudo-termp`
and also include an explicit notion of `null' term.

- Tterm-constant-list->value-list
- Lift
`tterm-constant->value`to lists. - Tterm-free-vars
- Set of free variables in a (translated) term.
- Maybe-tterm
- Fixtype of translated terms and
nil . - Tterm-constant-list
- Lift
`tterm-constant`to lists. - Tterm-case-constant-listp
- Lift
(tterm-case ... :constant) to lists. - Lift-term
- Lift pseudo-terms to the meta level.
- Tterms