diff options
| author |  Rustan Leino <unknown> | 2014-07-08 14:35:52 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2014-07-08 14:35:52 -0700 |
| commit | f0b0ac64dc1d45e87c4eec869991ed86d8439f7f (patch) | |
| tree | 3c95b6c5121e5c746cf7bdb740071ca8114d2b23 /Test/dafny0/ResolutionErrors.dfy | |
| parent | 61aa8c356946a60a1e68934a07faba89b95ff1ce (diff) | |
| parent | 79eae1e70e52bde8acfbfb2a09a0560c7319b224 (diff) | |
Merge
Diffstat (limited to 'Test/dafny0/ResolutionErrors.dfy')
| -rw-r--r-- | Test/dafny0/ResolutionErrors.dfy | 22 |
1 files changed, 22 insertions, 0 deletions
diff --git a/Test/dafny0/ResolutionErrors.dfy b/Test/dafny0/ResolutionErrors.dfy index 5b550339..137aa92c 100644 --- a/Test/dafny0/ResolutionErrors.dfy +++ b/Test/dafny0/ResolutionErrors.dfy @@ -961,3 +961,25 @@ method TypeConversions(m: nat, i: int, r: real) returns (n: nat, j: int, s: real j := int(j); // error: cannot convert int->int
j := int(n); // error: cannot convert nat->int
}
+
+// --- filling in type arguments and checking that there aren't too many ---
+
+module TypeArgumentCount {
+ class C<T> {
+ var f: T;
+ }
+
+ method R0(a: array3, c: C)
+
+ method R1()
+ {
+ var a: array3;
+ var c: C;
+ }
+
+ method R2<T>()
+ {
+ var a: array3<T,int>; // error: too many type arguments
+ var c: C<T,int>; // error: too many type arguments
+ }
+}
|