summaryrefslogtreecommitdiff
path: root/Test/dafny4/Bug67.dfy
blob: f12697135f68e1495d3ed5e3e3f5bd65f443873b (plain)
1
2
3
4
5
6
7
8
9
10
11
// RUN: %dafny /compile:3  "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

datatype d = D(m:seq<int>)

method Main()
{
  assert D([10, 20]) == D([10, 20]); // succeeds
  print [10, 20] == [10, 20], "\n"; // prints True
  print D([10, 20]) == D([10, 20]); // prints False
}