diff options
| author |  leino <unknown> | 2015-04-24 09:48:01 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-04-24 09:48:01 -0700 |
| commit | 84b3df3615af4f83df753b042b276b994a97b18b (patch) | |
| tree | f834b103760c740f0aa6d27f075343d9693cec9a /Test/dafny0/ResolutionErrors.dfy | |
| parent | 90c68ad369e3f9318d4f31ed4f9e628cb7f2738d (diff) | |
Fixed bug in tuples
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index f0138c6c..761cffa0 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -1342,3 +1342,10 @@ module GhostLet { x := ghost var a :| 0 <= a; 10; // fine
}
}
+
+// ------------------- tuple equality support -------------------
+
+module TupleEqualitySupport {
+ datatype GoodRecord = GoodRecord(set<(int,int)>)
+ datatype BadRecord = BadRecord(set<(int, int->bool)>) // error: this tuple type does not support equality
+}
|