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

Re: [tlaplus] tuples in function constructors using tlapm ?





On Wed, Apr 19, 2017 at 1:41 PM, Ioannis Filippidis <jfili...@xxxxxxxxx> wrote:

p == [t \in S \X S |-> << t[1], t[0] >> ]
THEOREM p = [t \in S \X S |-> << t[1], t[0] >> ]
    BY DEF p



A correction: the above should have been: t[2], t[1].

ioannis