blob: c433451cf3bdfd561e27da50c313629ceebe017f (
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 {:nowarn} :: x in (map [1:=10, 2:=20]) ==> x > 0), "\n";
}
|
