diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-19 00:52:14 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-19 00:52:14 -0700 |
| commit | 161e62b3f4e66fb1ebd94acb240c6b4a59acc640 (patch) | |
| tree | c9844ce7fa4ce7e65420ebcd5e87f0a3fba820e3 /Test/dafny0/NoTypeArgs.dfy | |
| parent | a7b7daf3290c5dc25a867f5ed24694758cec0ec1 (diff) | |
fixed and improved scheme for inferring type parameters
Diffstat (limited to 'Test/dafny0/NoTypeArgs.dfy')
| -rw-r--r-- | Test/dafny0/NoTypeArgs.dfy | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/Test/dafny0/NoTypeArgs.dfy b/Test/dafny0/NoTypeArgs.dfy index c41c7990..88418de7 100644 --- a/Test/dafny0/NoTypeArgs.dfy +++ b/Test/dafny0/NoTypeArgs.dfy @@ -80,3 +80,15 @@ ghost method Lemma(xs: List, ys: List) assert forall a, b, c :: concat(a, concat(b, c)) == concat(concat(a, b), c);
}
}
+
+// ------ Here are some test cases where the inferred arguments will be a prefix of the given ones
+
+method DoAPrefix<A, B, C>(xs: List) returns (ys: List<A>)
+{
+ ys := xs;
+}
+
+function FDoAPrefix<A, B, C>(xs: List): List<A>
+{
+ xs
+}
|