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

*From*: "'Chris Jensen' via tlaplus" <tlaplus@xxxxxxxxxxxxxxxx>*Date*: Mon, 08 Nov 2021 10:10:15 +0000*Ironport-hdrordr*: A9a23:VKvykqsP1cy2pJPANGnQyDAs7skCa4Mji2hC6mlwRA09TyXGraze5cjzhCWY+VAssS8b86HmBICrR3TA+ZlppawcOrm+XWDdySCVxeBZnPrfKljbdBEWmdQtoZuIH5IOe+EYSGIK+voTDmGDYpEdKPfuytHtuQ6c9QYscelSA5sQqjuRczzrVHGeJzM2TKbQofGnl4t6TkSbCAQqh5+Adzc4toH4zrWh5feWGW94dmAaBRG1/EiVAfzBYm6lN3ElInxyKNwZgB34emLCl9eeWzDS8G6/64YR1fVrcRnapOeqtKe3+4oow/nX6jpAHL4RE4FrsVsO0aySAIBAqqiBn//RVP4DoU85t1vFwmqI5yDQlAwJzF/JjXK7oV+mm+zWY1sBerB8rLMcSB3f60BlmP4U6tM240up86BPBReFtiXw7drFWlVLkQ6bunw/iIco/j9iud93Us4tkbAi*References*: <3ad9a5c4-d76f-4e8b-b670-e2378ee46155n@googlegroups.com>

Hi!

Thanks for the reply. The
specific set I want to define is inductively defined/constructed, with the
predicate being equivalent to a proof that the element is possible to
construct (in a prolog style fashion).

From the
linked summary, it doesn't seem that this is possible, however I read
somewhere that it was possible to overload values to use a Java module (see
Nat). Is there any documentation on how to do
this?

In the short term I'm planning on generating
a sufficiently large finite subset and hoping that values outside of it are
not
generated.

Thanks,

Chris

On Saturday 06 November 2021 11:27:02 AM (+00:00), Leslie Lamport wrote:

--

Thanks,

Chris

-- On Saturday 06 November 2021 11:27:02 AM (+00:00), Leslie Lamport wrote:

A predicate does not define a set. The TLA+ operators for constructing sets are listed under the "Sets" heading on the "Constant Operators" section of:https://lamport.azurewebsites.net/tla/summary-standalone.pdfIf the "set" you want to define cannot be expressed with them, it is probably not what mathematicians define to be a set.Leslie--On Friday, November 5, 2021 at 11:05:58 AM UTC-7 Chris Jensen wrote:Hi!

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

predicate).

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?

--

Thanks,

Chris

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/3ad9a5c4-d76f-4e8b-b670-e2378ee46155n%40googlegroups.com.

--

Thanks,

Chris

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/1636365615616.605710175.720244640%40aol.com.

**Follow-Ups**:**RE: [tlaplus] Re: Type checking and custom infinite sets***From:*'Leslie Lamport' via tlaplus

**References**:**[tlaplus] Re: Type checking and custom infinite sets***From:*Leslie Lamport

- Prev by Date:
**[tlaplus] The TLA+ Video Course, module AB2H: is there a mistype in SpecH?** - Next by Date:
**RE: [tlaplus] Re: Type checking and custom infinite sets** - Previous by thread:
**[tlaplus] Re: Type checking and custom infinite sets** - Next by thread:
**RE: [tlaplus] Re: Type checking and custom infinite sets** - Index(es):