# [tlaplus] How to express this set comprehension in TLA+?

• From: "hengx...@xxxxxxxxx" <hengxin0912@xxxxxxxxx>
• Date: Mon, 5 Apr 2021 02:34:35 -0700 (PDT)
• Ironport-hdrordr: A9a23:86ewJqEsbDy+JzL4pLqEzseALOonbusQ8zAX/mp2TgFYddHdqtC2kJ0gvyPcpT4NVBgb9+yoF7KHRRrnnqJdxYUKJ7+tUE3HtQKTQ71KyYvnz3neFzbl9uhbvJ0MT4FEBNf9DUd3gK/BiWGFOuw9y9qK+r3Av4vj5kpqJDsKV4hQqyNwCgOWCSRNJDV7OQ==

I want to express the following set comprehension (as a simplied example)

{<<x, y>> : x \in 1 .. 2, y \in 1 .. 2, y # x}

in TLA+ and expect the result {<<1, 2>>, <<2, 1>>}.
Note that the third condition "y # x" uses variable "x".

However, I got a parse error.

How should I correctly express it in TLA+?

Best regards,
hengxin

--
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+unsubscribe@xxxxxxxxxxxxxxxx.