# Re: [tlaplus] << >> = { }

Excuse me. No what is defined by IsAFcn is the operator [ x \in A |-> B ] not
IsAFcn. I had missed the equality.

For those who are interested, the property used by TLA+ to define a function would be in