|
|
|---|
|
|
|
|---|
Fixtype of translated terms.
This is a tagged union type, introduced by fty::deftagsum.
A translated term is a variable (any symbol), a (quoted) constant (of any value), or a function call. The latter consists of a function (see tfunction) and a list of zero or more argument terms. We do not constrain here the number of argument terms to match the number of formal parameters of the lambda expression, when the function is a lambda expression.
Note that, for variables, we use the symbol values formalized by symbol-value, not the ACL2 symbol. The reason is the one explained in symbol-value: we want to represent all possible variables, not just the ones that are valid for the current packages.