Hi Chris,
This sounds like a reasonable enhancement of the PlusCal language. We'll check that it doesn't change the translation of any files now accepted by the translator and will then take a look at what you have done. If it looks good, we'll add it to the next release. Thanks for the suggestion and the implementation.
By the way, the TLA+ specs of the translation say that they are valid only for the version of PlusCal at the date indicated at the beginning of the spec. I think those versions are now 10 years old and a number of changes have been made to PlusCal since then. I stopped keeping the specs up to date because I had too many other things to do. I didn't think there was too much point to keeping the specs current, since no one was going to use them to understand the semantics of PlusCal.
Leslie