I often find myself wanting to both map and filter at the same time, which requires the following somewhat cumbersome _expression_:
I think this would be much improved in readability if we had a language-level construct similar to:
This is similar to set comprehensions in Python, which is probably my favorite feature of that language.
EXCEPT support for nested functions
Many of the specs I write are of distributed systems, so I'll usually have one or more variables of this type:
When I want to update a single value in distributedData, I use this notation:
It would be nicer if we could write it something like this:
I recall this also as a common point of confusion among TLA+ course attendees, who intuitively tried this notation at first.
I'm not sure whether either of these suggestions violate some bedrock principle in the TLA+ construction (I could see that for the latter) but they certainly would both make my life simpler and reduce the cognitive overhead of reading/writing TLA+.
New standard module: Query
Not a fully fleshed-out idea, but it might be nice to have a new standard module that implements something like relational algebra for easy manipulation of sets of records, in addition to other common higher-level functions like fold and zip.
Anyone else have suggestions of their own?