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

Unconventional indeed. But what is defined here is the predicate IsAFcn not
the concept of function nor the operator [ x \in A |-> B ].

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

But unconventional anyway.

--
FL