[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[tlaplus] Type checking and custom infinite sets
- From: "'Chris Jensen' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>
- Date: Fri, 05 Nov 2021 18:05:50 +0000
- Ironport-hdrordr: A9a23:L5p1Nq0RnFpFgvIZc+Q/SgqjBIskLtp133Aq2lEZdPUCSL38qynIpoV46faUskdzZJhOo7q90cW7LE80sKQa3WBzB9eftWvd11dAd7sSibcKqgeIc0bDH4VmtJuIBpIObuEYemIK9PoSjjPVLz9Z+qjhzJyV
- References: <firstname.lastname@example.org>
When you have a type invariant for a system like Paxos, you can check that
for example ballot numbers are members of the set of natural numbers.
What I am trying to do (and can't seem to find any documentation on) is how
to define my own infinite sets (for example one which is defined by some
This is specifically just for type checking, and thus should just be
checking whether a value is an element of a set, hence should just be able
to use the predicate.
Is there any way to do this?
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/1636133961518.1536267474.2186325086%40aol.com.