diff options
| author |  Dan Rosén <danr@chalmers.se> | 2014-07-11 11:00:27 -0700 |
|---|---|---|
| committer | Dan Rosén <danr@chalmers.se> | 2014-07-11 11:00:27 -0700 |
| commit | d5d4ee8783543750993c5b18999bd8b099ad4ef7 (patch) | |
| tree | 1fdf272982f614fc1cc75e82335175212c2e1d78 /Test/dafny0/DisplayExpressions.dfy.expect | |
| parent | 3fa2caeb19bdd1b15cd0f3ffdd5d9acb4bbaaa8d (diff) | |
Check that type arguments to map display expressions are fully resolved
Also add a test case for the different display expressions.
Diffstat (limited to 'Test/dafny0/DisplayExpressions.dfy.expect')
| -rw-r--r-- | Test/dafny0/DisplayExpressions.dfy.expect | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/Test/dafny0/DisplayExpressions.dfy.expect b/Test/dafny0/DisplayExpressions.dfy.expect new file mode 100644 index 00000000..1867ff3a --- /dev/null +++ b/Test/dafny0/DisplayExpressions.dfy.expect @@ -0,0 +1,5 @@ +DisplayExpressions.dfy(5,11): Error: the type of this map constructor is underspecified, but it cannot be an arbitrary type. +DisplayExpressions.dfy(10,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type. +DisplayExpressions.dfy(15,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type. +DisplayExpressions.dfy(20,11): Error: the type of this collection constructor is underspecified, but it cannot be an arbitrary type. +4 resolution/type errors detected in DisplayExpressions.dfy |