Kukovec

@konnov @shonfeder @thpani @bugarela thoughts?

You'll never be able to define `IsSequence(seq)` the way you want and here's why: Russel's paradox demonstrates that there cannot be a "set of all sets" (you need a category)....

I just ran this today, and the error message reads: ``` Parsing error in the type annotation: () => (Bool, Bool) Typing input error: Parser error in type annotation of...

Closing this, we'll keep #943 for tracking error message UX.

Closing this, as it is effectively a duplicate of #468

Not present in the current version anymore.

```sh apalache-mc check --bogus=bogus test.tla ``` currently fails with ``` Failed to parse command check: No option found for --bogus=bogus ``` and no unhandled exception.

I looked at this today, and the problem arises way before this gets to the inliner. Essentially, ```tla LOCAL LocalOp(o) == VariantGetUnsafe("Foo", o) ... GetLocal(o) == LocalOp(o) ``` turns into...

We have a systematic approach, it's called "using the scoped builder".

But beyond that, as soon as any form of rewriting occurs, the only reasonable way to consistently avoid shadowing is to mangle all the names into unique, illegal-character prefixed strings.