[FEATURE] Standard module for Apalache

[konnov]

Following #181 and #157, we should finally introduce a standard module for Apalache that contains all handy operators, which until today have been introduced only by the Apalache transformations. We should expose these operators to the users, so they should be able to fix issues by hand. We have to expose all operators in BmcOper in Apalache.tla, except for probably <:, which should be introduced in its own module Types.tla.

@lemmy, is there any standard practice for distributing non-SANY modules, or shall we just expect the user to download Apalache.tla from a known location and keep it up to date?

[lemmy]

"Standard Modules" are those that appear in Specifying Systems. For other modules that have broad applicability, I've created https://github.com/tlaplus/CommunityModules/

[konnov]

Cool, I have opened an issue there. I think it is more of an issue for the SANY parser, but it is also related to the community libraries.