diff options
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 |