From e10098cde7bac9a7a1576000fa29d15f1fcd8970 Mon Sep 17 00:00:00 2001
From: Rustan Leino <unknown>
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/ResolveError.dfy | 34 +++++++++++++++++-----------------
 1 file changed, 17 insertions(+), 17 deletions(-)

(limited to 'Test/hofs/ResolveError.dfy')

diff --git a/Test/hofs/ResolveError.dfy b/Test/hofs/ResolveError.dfy
index 3c0d7cd9..ae838eb3 100644
--- a/Test/hofs/ResolveError.dfy
+++ b/Test/hofs/ResolveError.dfy
@@ -3,9 +3,9 @@
 
 
 method ResolutionErrors() {
-    var x;
-    var g5 := x, y => (y, x);   // fail at resolution
-    var g6 := x, (y => (y, x)); // fail at resolution
+  var x;
+  var g5 := x, y => (y, x);   // fail at resolution
+  var g6 := x, (y => (y, x)); // fail at resolution
 }
 
 // cannot assign functions
@@ -23,20 +23,20 @@ method Nope3() {
 
 method RequiresFail(f : int -> int)
   // ok
-  requires f(0) == 0;
-  requires f.requires(0);
-  requires f.reads(0) == {};
+  requires f(0) == 0
+  requires f.requires(0)
+  requires f.reads(0) == {}
 
   // fail
-  requires f(0) == true;
-  requires f(1,2) == 0;
-  requires f(true) == 0;
-  requires f.requires(true);
-  requires f.requires(1) == 0;
-  requires f.requires(1,2);
-  requires f.reads(true) == {};
-  requires f.reads(1) == 0;
-  requires f.reads(1,2) == {};
+  requires f(0) == true
+  requires f(1,2) == 0
+  requires f(true) == 0
+  requires f.requires(true)
+  requires f.requires(1) == 0
+  requires f.requires(1,2)
+  requires f.reads(true) == {}
+  requires f.reads(1) == 0
+  requires f.reads(1,2) == {}
 {
 }
 
@@ -56,7 +56,7 @@ method Bla() {
   assert Bool;
 }
 
-method Pli(f : A -> B) requires f != null;
+method Pli<A,B>(f : A -> B) requires f != null
 {
   var o : object;
   assert f != o;
@@ -102,7 +102,7 @@ module AritySituations {
     w := V;  // error
   }
 
-  method P(r: T -> U, x: T) returns (u: U)
+  method P<T,U>(r: T -> U, x: T) returns (u: U)
     requires r.requires(x);
   {
     u := r(x);
-- 
cgit v1.2.3