Shon Feder

Wow. Good find!

Ah, if the spec size is always small and we don’t have to do repeated lookups, then probably not worth it to optimize. Tho we might still want to use...

List map is good for ergonomics (we could ditch some other code, I think, like `BodyMap`), but it doesn't give constant time lookups.

Just realized I was wrong about these caching the sequences: iiuc, they compute the sequences on invocation. This mean that on each invocation we re-filter out the subset of relevant...

(of course, this is still just a micro optimization if we only ever have small numbers of declarations :) ).

Thanks for the report @craft095. Our parsing phase indeed doesn't interact with the type checking or inference. FYI, you can get the output from parsing or typechecking a bit easier...

I wonder if this should be viewed as a documentation bug? We could add a note in the CLI doc for `parse` like `Parse a TLA+ specification and quit (ignores...

To be sure that we can direct our advice and investigations in the right direction, I think it would help for us to be able to discuss in some concrete...

> Apalache and TLC share the same parser SANY, which is a problem, because I need some level of independence. So I am going to generate IR instead of TLA+...

@konnov said we shouldn't be allowing functions with infinite domain at all, and that he has a fix in mind, so will leave this until we can sync on Monday.