1 files changed, 0 insertions, 43 deletions
diff --git a/Test/dafny0/Comprehensions.dfy b/Test/dafny0/Comprehensions.dfy
deleted file mode 100644
index ca1fcfb7..00000000
--- a/Test/dafny0/Comprehensions.dfy
+++ /dev/null
@@ -1,43 +0,0 @@
-method M()
-{
-  var numbers := set i | 0 <= i && i < 100;
-  var squares := set i | 0 <= i && i < 100 :: Id(i)*i;  // verifying properties about set comprehensions with a term expression is hard
-
-  assert 12 in numbers;
-  assert Id(5) == 5;
-  assert 25 in squares;
-  assert 200 in numbers;  // error
-}
-
-function method Id(x: int): int { x }  // for triggering
-
-datatype D = A | B;
-// The following mainly test that set comprehensions can be compiled, but one would
-// have to run the resulting program to check that the compiler is doing the right thing.
-method Main()
-{
-  var q := set i,j | 0 <= i && i < 10 && 0 <= j && j < 3 :: i+j;
-  PrintSet(q);
-  q := set b: bool | true :: if b then 3 else 7;
-  var d := set b:D | true;
-  var test := forall d:D :: d == A || d == B;
-  PrintSet(q);
-  var m := set k | k in q :: 2*k;
-  PrintSet(m);
-  PrintSet(set k | k in q && k % 2 == 0);
-  var sq := [30, 40, 20];
-  PrintSet(set k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i);
-  var bb := forall k, i | k in sq && 0 <= i && i < k && i % 7 == 0 :: k + i == 17;
-}
-
-method PrintSet<T>(s: set<T>) {
-  var q := s;
-  while (q != {})
-    decreases q;
-  {
-    var x := choose q;
-    print x, " ";
-    q := q - {x};
-  }
-  print "\n";
-}