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