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

Re: [tlaplus] Checking whether something is a record or a set?

Just a thought:

If a Record is defined as a set of records (p. 28 in Specifying Systems), then

IsRecord(r) == r \in Record

should do the test.  I use this approach for my TypeInvariants.

Thank you,