[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

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.