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 | |
| 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')
| -rw-r--r-- | Test/dafny0/DisplayExpressions.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Test/dafny0/DisplayExpressions.dfy b/Test/dafny0/DisplayExpressions.dfy new file mode 100644 index 00000000..767cfcdb --- /dev/null +++ b/Test/dafny0/DisplayExpressions.dfy @@ -0,0 +1,21 @@ +// RUN: %dafny /compile:0 "%s" > "%t"
+// RUN: %diff "%s.expect" "%t"
+method M()
+{
+ var m := map[];
+}
+
+method N()
+{
+ var n := multiset{};
+}
+
+method O()
+{
+ var o := [];
+}
+
+method P()
+{
+ var p := {};
+}
|