quint: Example in "Namespaces and Imports" does not type check
The following example from the documentation
module Outer {
var x: int
def xPlus(z) = x + z
module Inner {
val x2 = x + x
}
val inv =
(Inner.x2 - x == x)
}
Does not type check.
About this issue
- Original URL
- State: closed
- Created a year ago
- Comments: 16 (14 by maintainers)
My bad. I copied the first example by mistake and stuck to it, but it is actually the second example. The issue is updated.
As a side problem, it does not work in REPL, as REPL does not support constants yet. The error message is using the outdated syntax: