"@@" and ":>"

[drrtal...@xxxxxxxxx]

Hi,

I'm working through the TLA+ Hyperbook and in the section on function, 15.2, the operators "@@" and ":>" are used. What are these operators called (i.e., their spoken names, if you will)? 

The ":>" operator is a mapping operator, mapping a single value from one set into a single value in another value. 

The effect of the "@@" operator combines the domains of two functions and yields the value that corresponds an element of that union, but favoring the first of the two functions whenever both have that element in their respective domains. 

Thanks,

Roger Alexander.