{"action":"opened","issue":{"url":"https://api.github.com/repos/tlaplus/v2-tlapm/issues/7","repository_url":"https://api.github.com/repos/tlaplus/v2-tlapm","labels_url":"https://api.github.com/repos/tlaplus/v2-tlapm/issues/7/labels{/name}","comments_url":"https://api.github.com/repos/tlaplus/v2-tlapm/issues/7/comments","events_url":"https://api.github.com/repos/tlaplus/v2-tlapm/issues/7/events","html_url":"https://github.com/tlaplus/v2-tlapm/issues/7","id":243906638,"number":7,"title":"Improving support for functions of multiple arguments","user":{"login":"johnyf","id":3135273,"avatar_url":"https://avatars0.githubusercontent.com/u/3135273?v=4","gravatar_id":"","url":"https://api.github.com/users/johnyf","html_url":"https://github.com/johnyf","followers_url":"https://api.github.com/users/johnyf/followers","following_url":"https://api.github.com/users/johnyf/following{/other_user}","gists_url":"https://api.github.com/users/johnyf/gists{/gist_id}","starred_url":"https://api.github.com/users/johnyf/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/johnyf/subscriptions","organizations_url":"https://api.github.com/users/johnyf/orgs","repos_url":"https://api.github.com/users/johnyf/repos","events_url":"https://api.github.com/users/johnyf/events{/privacy}","received_events_url":"https://api.github.com/users/johnyf/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2017-07-19T02:41:27Z","updated_at":"2017-07-19T02:41:27Z","closed_at":null,"body":"This is a [known issue](https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Unsupported_features.html) (related to tuples) mentioned here in order to document it and associate to other issues. Examples for `tlapm` v1.4.3:\r\n\r\n- `tlapm` does not parse the unsupported syntax: `[<< a, b >> \\in S |-> TRUE]`.\r\n- `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.\r\n\r\n```tla\r\n------------------------------- MODULE test --------------------------------\r\nCONSTANT S\r\n\r\n(* `tlapm` cannot prove the following theorem. *)\r\ng == [a, b \\in S |-> TRUE]\r\nTHEOREM g = [a, b \\in S |-> TRUE]\r\n    BY DEF g\r\n\r\n\r\n(* For comparison, `tlapm` can prove the following claims: *)\r\nh == [a \\in S |-> TRUE]\r\nTHEOREM h = [a \\in S |-> TRUE]\r\n    BY DEF h\r\n\r\n\r\np == [t \\in S \\X S |-> << t[1], t[2] >> ]\r\nTHEOREM p = [t \\in S \\X S |-> << t[1], t[2] >> ]\r\n    BY DEF p\r\n================================================================================\r\n```\r\n\r\n`tla2sany test.tla` confirms that the module `test` is well formed, but `tlapm` raises:\r\n\r\n```isabelle\r\nError: Could not prove or check:\r\n         ASSUME NEW CONSTANT S,\r\n                g == [a, b \\in S |-> TRUE]\r\n         PROVE  g = [a, b \\in S |-> TRUE]\r\n```\r\n\r\nThis issue appears to be relevant to #5 and #6."}}
{"actor":{"display_login":"johnyf"}}