[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [tlaplus] Examples of specs with proofs that use subexpressions?
- From: Andrew Helwer <andrew.helwer@xxxxxxxxx>
- Date: Mon, 26 Apr 2021 14:03:30 -0700 (PDT)
- Ironport-hdrordr: A9a23:AUdtLqtd2AaooQpdYROkLQEC7skC2YMji2hD6mlwRA09T+WzkceykPMHkSLlkTp5YgBdpfmsGomlBUnd+5l8/JULMd6ZNmTbkUahMY0K1/qH/xTOACv7n9QtsptIU687M9HoCEg/sMCS2njBL/8EwMObtIiyj+bf0HsFd3AdV4hE7x1lTieWF1QefngwObMdFICAouprzgDQCkg/S8SgGz09WfLfzue74K7ORB4dGloa7xOThimj877wH3Gjr14jehdu5ZtnzmTfiQz+4cyYwoyG4zvV12rS6JoTndv617J4dbyxo+wYMC/lhArtRIkJYcz6gBkNu+2k5Fsnl9PByi1QTvhb0H/acmGrrRaF4WCJu0dN11bYxVCVmnflq8DiLQhKcPZpvo5Bdwuc1kxIhqAD7Itw02WVu4E/N3z9tR7g7NvFXQwCrDvPnVMel4co/hpieLpbQ7NcqrEf8FhYea1wfx7S2cQIFK1LANvH7PhbNWmGZ23U11MA/PWcGlo0GBmCTgwumOywlwJXkndw0lcCyKUk8ksoxdYSTZ9L4uiBHL9viKgLbsJ+V9MJOM4xBeWwDGLJTVb3NH+KZW7gCLoMNxv2yqLf0fES/+GleJsByd8JlJPNXEgwjx9MR2veTfaD1pFK7RzBKV/cLFHQ4/Ab3YFwvvnXRbbgMyGPDHAo1+W6pekHa/erKcqOBA==
- References: <firstname.lastname@example.org> <CAFteovJe664o=A=oTy+jjjeDbQ=69Asfg3C5dUSCODzvY_KPQQ@mail.gmail.com>
By subexpressions I mean stuff like foo(2, 3)!bar!<<!(1)!:!>>, which you can use to refer to specific parts of a larger _expression_. The linked proof does use subexpressions in a limited way, to bind quantifiers, but not in a more involved way.
On Monday, April 26, 2021 at 2:07:39 PM UTC-4 k.petr...@xxxxxxxxx wrote:
Do you mean such an example?
Don't know if that works in TLC.
Been reading the TLA+2 language spec and had no idea that subexpressions existed and were so powerful. You can use the language itself to navigate around the parse tree of the TLA+ file you're working in! Are there any examples of TLAPS proofs which use this? Also, does TLC support it (although I assume it's quite inefficient)?
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/88d70b38-4c59-4134-9112-fb993521923fn%40googlegroups.com.