SANY should indicate if a module it uses is a built-in one

[lemmy]

xxyzzn:

A flag should be aded to modules which are built-in and are loaded by SANY from a specific folder. This information is required for the PM in order to overide the symbols. For example, the Integer.tla module should, if loaded from the pre-configured location, be labelled with "dummy=true" or "build-in=true" in the SANY syntax tree.

libal:

I just confirmed that the SANY parser reports the operators in Naturals, TLAPS and other library modules with kind UserDefinedOpKind. Since these operators have fixed semantics, it would be nice to have them under kind BuiltInKind.

xxyzzn:

The operators in Naturals, etc. are not built-in operators, so it would be very un-nice if SANY reported them as such. For example, it would make it impossible for the user to have TLC override the definition of the operator Seq from the Sequences module.

xxyzzn:

A field named isStandard that indicates if the module is a standard module was added to the ModuleNode class in the version of the code I just committed.

[lemmy]

Do not see an actionable item, thus closing. Please reopen if necessary.