TLAPM parser incorrectly allows LAMBDA as expression #238
Description
Found during work on #229; TLAPM should reject this parse input, as LAMBDAs are only allowed in particular places (generally, as parameters to other operators):
---- MODULE Test ----
op == LAMBDA x : 0
====SANY correctly rejects this input.
As in #237, this has to do with how the parse tree represents operators with parameters. When expanding an Expr.T.defn variant and matching it to an Operator (name : Util.hint, expr : Expr.T.expr) instance, operators with parameters are represented by expr matching to a Lambda variant. This isn't inherently bad unless you're a "make invalid state unrepresentable" hardliner, since the parser could just reject LAMBDAs occurring in places where expressions are required while assembling operator definitions as described. However, the parser does not check for that and so allows LAMBDAs in places where only expressions should be. This allowance is very general; expressions like 1 + LAMBDA x : 0 are accepted.