[FEATURE] Support LAMBDA in typecheck

[konnov]

Several specifications in the examples repository are using the LAMBDA-syntax. For instance, SlidingPuzzles defines the operator move(p, d) as follows (the type annotations are introduced by me):

move(p, d) == "(<<Int, Int>>, <<Int, Int>>) => <<Int, Int>>" :>
              LET s == "<<Int, Int>>" :>
                    <<p[1] + d[1], p[2] + d[2]>>
                  pc == ChooseOne(board, LAMBDA pc : s \in pc)
              IN <<pc, {<<q[1] - d[1], q[2] - d[2]>> : q \in pc}>>

The type checker produces the following error:

[SlidingPuzzlesTyped.tla:47:42-47:61]: Undefined name LAMBDA. Introduce a type annotation.

Currently, the type checker just ignores the LAMBDA syntax. It probably can be just substituted with a LET-IN definition. In this case, the type checker would automatically infer the types inside LAMBDA.

[konnov]

It is working already in unstable. Nothing to fix.