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";
}
|