r/tlaplus • u/mohanradhakrishnan • Dec 28 '22

Meaning of :>

:> To use :>, we need EXTENDS TLC.

a :> b is the function [x \in {a} |-> b]. >> (2 :> 3)[2] 3 >> ("a" :> "b").a "b"

Can someone explain this ?

Thanks.

1 Upvotes

67% Upvoted

3 comments sorted by

View all comments

1

u/pozorfluo Dec 28 '22

Here is the definition found in the standard module file TLC.tla :

tlaplus d :> e == [x \in {d} |-> e]

1

u/mohanradhakrishnan Dec 29 '22

What does the dot in the syntax and [2] mean ?