Hi Ioannis,as you noticed (and as stated on the Web site), the parser of the PM rejects any bindings involving tuples, such as    \E <> \in S : ...   or    { ... : <> \in S }The next major release of TLAPS will be based on the SANY parser, so this limitation will disappear, but we don't know yet when the release will be ready.Additionally, the backends currently have extremely poor support for functions that take more than one argument, such as in your exampleg == [a, b \in S |-> TRUE]THEOREM g = [a, b \in S |-> TRUE]    BY DEF gIf you look at the messages in the TLAPM console, you'll see that SMT, Zenon and Isabelle all complain about unsupported constructs. For the moment, I recommend as a workaround that you use "curried" functions instead and replace   [a,b \in S |-> TRUE]   by   [a \in S |-> [b \in S |-> TRUE]]and similarly  [S \X T -> U]   by   [S -> [T -> U]]Thanks for reminding us about this issue, which has been on our to-do list for too long already ...Regards,StephanOn 19 Apr 2017, at 22:41, Ioannis Filippidis wrote:This question seems to be answered by the documentation about partially supported features [1],but I would like to confirm I am not doing something wrongly.tlapm does not parse syntax of the form: [<< a, b >> \in S |-> TRUE], so it appears to be unsupported.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 below. Is such syntax unsupported by tlapm == 1.4.3?Does the development version of tlapm support syntax of this form?Searching through the repository for usage of |->, I couldn't find any example of this form, except for a comment [2].[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html[2] https://github.com/tlaplus/v2-tlapm/blob/fd345f78c7e356b53c67e24f17e99df449d7b3a3/src/oldpm/expr.ml#L81Best regards,ioannis------------------------------- MODULE test --------------------------------(* tlapm --version   1.4.3 (build 34695)*)CONSTANT S(* tla2sany test.tla confirms that the theorem below is well formed (p.304).tlapm -v -C test.tla raises:File "./test.tla", line 3, character 8required expressions(s) missing before '['File "":Error: Could not parse "./test.tla" successfully. tlapm ending abnormally with Failure("Module.Parser.parse_file")*)(*f == [<< a, b >> \in S |-> TRUE]THEOREM f = [<< a, b >> \in S |-> TRUE]    BY DEF f*)(* The below is well formed too, 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]*)g == [a, b \in S |-> TRUE]THEOREM g = [a, b \in S |-> TRUE]    BY DEF g(* tlapm can prove the following claims. *)h == [a \in S |-> TRUE]THEOREM h = [a \in S |-> TRUE]    BY DEF hp == [t \in S \X S |-> << t[1], t[0] >> ]THEOREM p = [t \in S \X S |-> << t[1], t[0] >> ]    BY DEF p================================================================================ -- You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@xxxxxxxxxxxxxxxx. To post to this group, send email to tla...@xxxxxxxxxxxxxxxx. Visit this group at https://groups.google.com/group/tlaplus. For more options, visit https://groups.google.com/d/optout.