diff options
Diffstat (limited to 'Test/dafny0')
| -rw-r--r-- | Test/dafny0/Modules0.dfy | 12 | ||||
| -rw-r--r-- | Test/dafny0/Modules0.dfy.expect | 3 |
2 files changed, 14 insertions, 1 deletions
diff --git a/Test/dafny0/Modules0.dfy b/Test/dafny0/Modules0.dfy index dbbffd87..4b86d848 100644 --- a/Test/dafny0/Modules0.dfy +++ b/Test/dafny0/Modules0.dfy @@ -335,3 +335,15 @@ module TopLevelStatics { static method M() // error/warning: static keyword does not belong here
{ }
}
+
+module Library {
+ class T { }
+}
+
+module AA {
+ import opened Library
+}
+
+module B refines AA {
+ datatype T = MakeT(int) // illegal
+}
diff --git a/Test/dafny0/Modules0.dfy.expect b/Test/dafny0/Modules0.dfy.expect index e4b46cce..f51e0f6c 100644 --- a/Test/dafny0/Modules0.dfy.expect +++ b/Test/dafny0/Modules0.dfy.expect @@ -30,5 +30,6 @@ Modules0.dfy(320,11): Error: Undeclared top-level type or type parameter: Wazzup Modules0.dfy(321,17): Error: module 'Q_Imp' does not declare a type 'Edon'
Modules0.dfy(323,10): Error: new can be applied only to reference types (got Q_Imp.List<?>)
Modules0.dfy(324,30): Error: member Create does not exist in class Klassy
+Modules0.dfy(348,11): Error: a datatype declaration (T) in a refinement module can only replace an opaque type declaration
Modules0.dfy(101,14): Error: Undeclared top-level type or type parameter: MyClassY (did you forget to qualify a name or declare a module import 'opened?')
-31 resolution/type errors detected in Modules0.dfy
+32 resolution/type errors detected in Modules0.dfy
|