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

[tlaplus] Record Equality

Hi,

I'm running TLAPS 1.6 (TLAPM 1.4.3) and the following is discharged by the proof system. Is this expected or a bug?

LEMMA RecordEquality == \A d1, d2 \in [slot: Nat]:
        /\ d1.slot = d2.slot
        /\ d1.val = d2.val
        => d1 = d2 BY Isa

Thanks,
Saksham

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJSuO--qCj9PrYf4riCOiwB71%2BusQ%3DXgVTO-Y4wkcQxfNG-qJw%40mail.gmail.com.