Added it on my bugfix list as next :)
For the multiline LET-IN definitions, there is an easy workaround, e.g., we can rewrite the above example as: ``` LET \* @type: Set(a -> b); F0 == F[n - 1]...
> Fundamentally, I don't care where z3 is coming from. We have to care, as the z3 team is breaking their APIs from time to time.
I am not sure what to do about it. It does not look like a high priority issue. Do you need it for an installation in an AWS instance?
> \* Super lucky that the unbounded CHOOSE picks an element that happens to match Seq(Int) There is no way to select a reasonable type signature for unbounded `CHOOSE`. So...
Before we go in automating anything, let's write HOWTOs: #546
Right. Now Apalache is expecting an operator name like `Next`. A similar issue has been raised by @Quantifier
This actually works right, at least for the state invariants. The output may be confusing though.
One issue is that the type checker is working at the level of `EtcExpr`, which lacks information about the original expressions. I think it makes sense to introduce another pass...
We are talking about `ConstInit` here. It should have complained about `x` being a variable, right?