From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Thu, 2 Jul 2015 16:06:02 -0700 Subject: 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. --- Test/hofs/Fold.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Test/hofs/Fold.dfy') 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, unit : B, f : (A,B) -> B): B +function method Fold(xs : List, unit : B, f : (A,B) -> B): B reads f.reads; requires forall x, y :: x < xs ==> f.requires(x,y); { -- cgit v1.2.3