1 files changed, 44 insertions, 0 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy
index 3f57f369..794f2f95 100644
--- a/Test/dafny0/TypeParameters.dfy
+++ b/Test/dafny0/TypeParameters.dfy
@@ -19,3 +19,47 @@ class C<U> {
 
   function G<Y>(): Y;
 }
+
+class SetTest {
+  method Add<T>(s: set<T>, x: T) returns (t: set<T>)
+    ensures t == s + {x};
+  {
+    t := s + {x};
+  }
+
+  method Good()
+  {
+    var s := {2, 5, 3};
+    call t := Add(s, 7);
+    assert {5,7,2,3} == t;
+  }
+
+  method Bad()
+  {
+    var s := {2, 50, 3};
+    call t := Add(s, 7);
+    assert {5,7,2,3} == t;  // error
+  }
+}
+
+class SequenceTest {
+  method Add<T>(s: seq<T>, x: T) returns (t: seq<T>)
+    ensures t == s + [x];
+  {
+    t := s + [x];
+  }
+
+  method Good()
+  {
+    var s := [2, 5, 3];
+    call t := Add(s, 7);
+    assert [2,5,3,7] == t;
+  }
+
+  method Bad()
+  {
+    var s := [2, 5, 3];
+    call t := Add(s, 7);
+    assert [2,5,7,3] == t || [2,5,3] == t;
+  }
+}