Improving support for functions of multiple arguments

[johnyf]

This is a known issue (related to tuples) mentioned here in order to document it and associate to other issues. Examples for tlapm v1.4.3:

• tlapm does not parse the unsupported syntax: [<< a, b >> \in S |-> TRUE].
• tlapm parses [a \in S, b \in S |-> TRUE] and [a, b \in S |-> TRUE], but it does not prove equality, as shown in the module test below.

------------------------------- MODULE test --------------------------------
CONSTANT S

(* `tlapm` cannot prove the following theorem. *)
g == [a, b \in S |-> TRUE]
THEOREM g = [a, b \in S |-> TRUE]
    BY DEF g


(* For comparison, `tlapm` can prove the following claims: *)
h == [a \in S |-> TRUE]
THEOREM h = [a \in S |-> TRUE]
    BY DEF h


p == [t \in S \X S |-> << t[1], t[2] >> ]
THEOREM p = [t \in S \X S |-> << t[1], t[2] >> ]
    BY DEF p
================================================================================

tla2sany test.tla confirms that the module test is well formed, but tlapm raises:

Error: Could not prove or check:
         ASSUME NEW CONSTANT S,
                g == [a, b \in S |-> TRUE]
         PROVE  g = [a, b \in S |-> TRUE]

This issue appears to be relevant to #5 and #6.