formal-methods

See https://github.blog/2022-05-09-supercharging-github-actions-with-job-summaries/

Instead of (or in addition to) posting a comment on the PR, we could generate a nice looking summary by emitting the Markdown content.

The TlaDocumentSymbolsProvider stumbles on operators while parsing constants and doesn't report them as model symbols. As a result, const operator names don't appear in the outline panel and in completion suggestions. Such operators also prevent parsing of the following constants.

A simple case:

CONSTANT Foo(_), Bar

Neither Foo nor Bar makes it to the model symbols list