{ (0 :> 2 @@ 1 :> 2),
(0 :> 2 @@ 1 :> 3),
(0 :> 3 @@ 1 :> 2),
(0 :> 3 @@ 1 :> 3) }
(0 :> 2 @@ 1 :> 2) \* is a function from the set above
(0 :> 2 @@ 1 :> 2) \in [ {0, 1} -> {2, 3} ] \* evals to TRUE
(0 :> 2 @@ 1 :> 2)[1] \* evaluates to 2
<<3,2,1>>[1] \* sequence/ tuple is a function so this evals to 3
So far makes sense.
Now...
(0 :> 2 @@ 1 :> 2) \* What is function?
I am under impression that function is set of one-to-one relations. Which it does look like. So it is a set, but not a proper TLA+ set? E.g. I cannot do this:
SUBSET (0 :> 2 @@ 1 :> 2)
Thank you!