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

Re: [tlaplus] meaning of the lead to (~>) operator

Is there a gauge on how widespread this issue is? The ~> operator seems to work as expected with some state predicates and not others...

Isaac DeFrain


On Wed, Apr 14, 2021 at 12:18 PM Isaac DeFrain <isaacdefrain@xxxxxxxxx> wrote:
Great! Thanks, Markus.

Isaac DeFrain


On Wed, Apr 14, 2021 at 12:16 PM Markus Kuppe <tlaplus-google-group@xxxxxxxxxxx> wrote:
On 14.04.21 11:14, Isaac DeFrain wrote:
> I now understand the issue you are encountering, Seup, as I am also
> encountering the same issue with ~> in a spec. This must be a bug in TLC.

https://github.com/tlaplus/tlaplus/issues/604

Markus

--
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/531db585-55d1-b729-0961-8c0d1877d8d4%40lemmster.de.

--
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/CAM3xQxGRpW49e_MtWi-Jju0-92nb4X10ovveoe0NvWSr1EugLg%40mail.gmail.com.