diff options
| author |  Rustan Leino <unknown> | 2015-07-02 16:06:02 -0700 |
|---|---|---|
| committer | Rustan Leino <unknown> | 2015-07-02 16:06:02 -0700 |
| commit | e10098cde7bac9a7a1576000fa29d15f1fcd8970 (patch) | |
| tree | 424cc0d382c4f870fa133c18228809da4d6a1bea /Test/hofs/Fold.dfy | |
| parent | c7f6887e452cbb91a8297bb64db39a8066750351 (diff) | |
Type parameters in method/function signatures are no longer auto-declared. Although
convenient and concise, the auto-declare behavior has on many occasions caused
confusion when a type name has accidentally been mistyped (and Dafny had then
accepted and auto-declared the name).
Note, the behavior of filling in missing type parameters is still supported. This
mode, although unusual (even original?) in languages, is different from the auto-
declare behavior. For auto-declare, identifiers could be used in the program
without having a declaration. For fill-in parameters, the implicitly declared
type parameters remain anonymous.
Diffstat (limited to 'Test/hofs/Fold.dfy')
| -rw-r--r-- | Test/hofs/Fold.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/hofs/Fold.dfy b/Test/hofs/Fold.dfy index 6ca2d3b1..9bcd9e02 100644 --- a/Test/hofs/Fold.dfy +++ b/Test/hofs/Fold.dfy @@ -13,7 +13,7 @@ function method Eval(e : Expr): int case Lit(i) => i } -function method Fold(xs : List<A>, unit : B, f : (A,B) -> B): B +function method Fold<A,B>(xs : List<A>, unit : B, f : (A,B) -> B): B reads f.reads; requires forall x, y :: x < xs ==> f.requires(x,y); { |