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)

Most upvoted comments

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:

compile error: <input>:8:5 - error: Assignment <- needs two arguments