Picked this up from a new submodule added to the tlaplus/examples repo:
https://github.com/tlaplus/azure-cosmos-tla/blob/4b8785a36ed16faa2cd1bd78b89e224d71711ee3/scenario1/swscop.tla#L34
Both pcal.trans and tla2sany.SANY accept this syntax. At first glance I think the grammar wants there to be curly braces, but they're elided here.
@susliko would you be able to take a look when you have time?
Picked this up from a new submodule added to the tlaplus/examples repo:
https://github.com/tlaplus/azure-cosmos-tla/blob/4b8785a36ed16faa2cd1bd78b89e224d71711ee3/scenario1/swscop.tla#L34
Both
pcal.transandtla2sany.SANYaccept this syntax. At first glance I think the grammar wants there to be curly braces, but they're elided here.@susliko would you be able to take a look when you have time?