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

// This method can be used to test compilation.
method Main()
{
    var s := {2, 3};
    var m := map[2 := 20, 3 := 30];
    print (s, m), "\n";
    print (|s|, |m|), "\n";
    print(set s | s in m), "\n";
    print (forall x :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
}