diff options
| author |  qunyanm <unknown> | 2016-03-21 11:45:14 -0700 |
|---|---|---|
| committer | qunyanm <unknown> | 2016-03-21 11:45:14 -0700 |
| commit | a89b9aee05dff74345a79f8fb4fe0fe3fdbb17ad (patch) | |
| tree | 251401e34f6ddbc73623e63f3f6d6637b2d0d088 /Test/dafny0/ModuleExport.dfy | |
| parent | acbc126c01fee3ab71647a7b16f4dcfc80eee2ea (diff) | |
Update module export error messages. Also for "import Y" if there is at least
one exported view, but no exported view is marked as default, then it is an
error.
Diffstat (limited to 'Test/dafny0/ModuleExport.dfy')
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy | 37 |
1 files changed, 37 insertions, 0 deletions
diff --git a/Test/dafny0/ModuleExport.dfy b/Test/dafny0/ModuleExport.dfy index 81fe0ed5..1e69764f 100644 --- a/Test/dafny0/ModuleExport.dfy +++ b/Test/dafny0/ModuleExport.dfy @@ -65,4 +65,41 @@ module E { case Kiwi(x) => 7
case Orang => 8 // error
}
+}
+
+module F {
+ default export Public { f, h}
+ default export E1 { f, g}
+ export E2 extends Public2, E1 {T} // error: Public2 is not a exported view of F
+ export Friend extends Public {g2, T} // error: g2 is not a member of F
+ export Fruit {Data}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+
+ class T
+ {
+ static method l() {}
+ }
+
+ datatype Data = Lemon | Kiwi(int)
+}
+
+module G {
+ export Public { f, h}
+
+ method h() {}
+ function f(): int { 818 }
+ function g() : int { 819 }
+ function k() : int { 820 }
+}
+
+module H {
+ import G // error: G has no default export
+}
+
+module I {
+ import G.Public // OK
}
\ No newline at end of file |