diff options
Diffstat (limited to 'Test/dafny0/ModuleExport.dfy.expect')
| -rw-r--r-- | Test/dafny0/ModuleExport.dfy.expect | 13 |
1 files changed, 13 insertions, 0 deletions
diff --git a/Test/dafny0/ModuleExport.dfy.expect b/Test/dafny0/ModuleExport.dfy.expect new file mode 100644 index 00000000..274c8f31 --- /dev/null +++ b/Test/dafny0/ModuleExport.dfy.expect @@ -0,0 +1,13 @@ +ModuleExport.dfy(30,11): Error: unresolved identifier: g
+ModuleExport.dfy(31,11): Error: unresolved identifier: k
+ModuleExport.dfy(32,4): Error: unresolved identifier: T
+ModuleExport.dfy(32,7): Error: expected method call, found expression
+ModuleExport.dfy(42,11): Error: unresolved identifier: k
+ModuleExport.dfy(52,9): Error: unresolved identifier: g
+ModuleExport.dfy(53,9): Error: unresolved identifier: k
+ModuleExport.dfy(66,2): Error: member Orang does not exist in datatype Data
+ModuleExport.dfy(70,7): Error: Public2 must be an export of F to be extended
+ModuleExport.dfy(74,9): Error: g2 must be a member of F to be exported
+ModuleExport.dfy(70,7): Error: more than one default export declared in module F
+ModuleExport.dfy(90,7): Error: no default export declared in module: G
+12 resolution/type errors detected in ModuleExport.dfy
|