summaryrefslogtreecommitdiff
path: root/Test/dafny0/ModuleExport.dfy.expect
blob: 274c8f31d04611b25864910975bff2862a5dbb88 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
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