diff options
| author |  Rustan Leino <unknown> | 2013-02-11 19:50:57 -0800 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2013-02-11 19:50:57 -0800 |
| commit | 2c74f9200db870814ea3dae63484cbe969ec3526 (patch) | |
| tree | 26c83369d254a707b80726f63cf350d593a59737 /Test/dafny0/ResolutionErrors.dfy | |
| parent | e0f4d19e19d3cd09acaaec91bef529fc49d0c378 (diff) | |
Report error if type of a quantified variable cannot be inferred
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 69b8ea38..6c86e7a8 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -513,3 +513,22 @@ method LetSuchThat(ghost z: int, n: nat) x := var w := 2*w; w; // error: the 'w' in the RHS of the assignment is not in scope
ghost var xg := var w :| w == 2*w; w;
}
+
+// ------------ quantified variables whose types are not inferred ----------
+
+module NonInferredType {
+ predicate P<T>(x: T)
+
+ method NonInferredType0(x: int)
+ {
+ var t;
+ assume forall z :: P(z) && z == t;
+ assume t == x; // this statement determined the type of z
+ }
+
+ method NonInferredType1(x: int)
+ {
+ var t;
+ assume forall z :: P(z) && z == t; // error: the type of z is not determined
+ }
+}
|