summaryrefslogtreecommitdiff
path: root/Test/dafny0/ModulesCycle.dfy
blob: a7f1caa2cd8c3bb26fd1747ac849ab352ca670e9 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
module M {
  class T { }
  class U { }
}

module N {
}

module U imports N {
}

module V imports T {  // error: T is not a module
}

module A imports B, M {
  class Y { }
}

module B imports N, M {
  class X { }
}

module G imports A, M, A, H, B {  // error: cycle in import graph
}

module H imports A, N, I {
}

module I imports J {
}

module J imports G, M {
}