diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-09-26 00:09:04 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-09-26 00:09:04 -0700 |
| commit | 225930765d1f6c11dcf6c523ce0730457c07ec47 (patch) | |
| tree | 5ea7ecbd4e5a972ea27c64dc5a6f1004647603fc /Test/dafny0/IteratorResolution.dfy | |
| parent | 3aac24b3f84b0c969e08a13aee01c75457c43851 (diff) | |
Dafny: compile iterators
Diffstat (limited to 'Test/dafny0/IteratorResolution.dfy')
| -rw-r--r-- | Test/dafny0/IteratorResolution.dfy | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/Test/dafny0/IteratorResolution.dfy b/Test/dafny0/IteratorResolution.dfy index f45dd764..fe9e2563 100644 --- a/Test/dafny0/IteratorResolution.dfy +++ b/Test/dafny0/IteratorResolution.dfy @@ -72,6 +72,8 @@ module Mx { } else {
var x: int := h1.t; // error: h1 would have to be a GenericIteratorResult<int>
}
+
+ var h2 := new GenericIteratorResult; // error: constructor is not mentioned
}
}
|