QuintIR -> ApalacheIR

[shonfeder]

We need the type of operator declarations before we can convert them into tla
operator declarations.

TlaOperDecl requires a list of OperParams.
These are just pairs of the paramter name and it's arity (values have arity
0). To determine the arity of a parameter to a tnt operator def will require
inspecting the type inferred/checked for the operator.

The scoped builder also requires each parameter to be typed
separately, which again means
we'll need to inspect an operator declaration's type recover
the types for each parameter.

We cannot construct TLA operator declarations until we have the
types of the Quint operator declarations available. Whereas type annotations for
variables and constants in required, they are optional for operator
declarations, so as a rule we are not getting the types in the AST.

Thus, the following are pre-requisites for this issue

• Output typing map informalsystems/quint#345
• tnt Types -> Apalache Types informalsystems/quint#349
• Convert Quint expressions and operator defs to ApalacheIR #2351
• Convert Quint constants, variables, and and assumptions #2363
• Plan Conversion of Quint buitins #2364
• Convert Quint type defs #2365

[shonfeder]

this has become superseded by the factored Out issues, and we don't need it for tracking when we have the milestone