I'm sorry, but I have to come back at this. I know that the general sentiment is not to fix things that are not broken, but if a community member would perform the necessary changes, would there be any chance a pull request is merged?
In defense of the rule update for functions (feel free to skip depending on how opposed you are to the idea):
Doing so is possible and reasonable. Take for example the proposition <<1,"2">> # <<2,2>>.
- Even if the exact set representation of functions is unspecified, the existence of some (infinitely many) that respect the proposition seems intuitive (not a good argument, I know).
- Common definitions of functions (though not necessarily compatible with TLA) agree on the validity of the proposition. In particular, TLAPS can prove it.
- It simplifies some tasks, such as the definition of complex, comparable structures.
I'm not promising I will do it, but I have finally overcome the reluctance of looking at sources of large projects for the first time and took a little dive into the TLAplus repo. I think I have an approach that would not only lead to a reasonably simple implementation of the new rule but also simplify existing code by unifying comparison and equality and eliminating unnecessary reimplementations of those methods for similar classes without compromising their optimizations.
In case of a positive answer, I will open a new issue on GitHub and link this conversation. This way, people know it's been suggested and approved but has to come from the community, similar to the proper handling of strings.
Cheers,
Benjamin
On Wednesday, July 28, 2021 at 8:18:35 PM UTC+2 Leslie Lamport wrote: