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/Simple.dfy | 20 ++++++++++----------
 1 file changed, 10 insertions(+), 10 deletions(-)

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

diff --git a/Test/hofs/Simple.dfy b/Test/hofs/Simple.dfy
index c27fa82c..6d98531e 100644
--- a/Test/hofs/Simple.dfy
+++ b/Test/hofs/Simple.dfy
@@ -50,7 +50,7 @@ method Main() {
 }
 
 function method succ(x : int) : int
-  requires x > 0;
+  requires x > 0
 {
   x + 1
 }
@@ -74,24 +74,24 @@ method Main3() {
 }
 
 
-function P(f: A -> B, x : A): B
-  reads (f.reads)(x);
-  requires (f.requires)(x);
+function P<A,B>(f: A -> B, x : A): B
+  reads (f.reads)(x)
+  requires (f.requires)(x)
 {
   f(x)
 }
 
 
-function Q(f: U -> V, x : U): V
-  reads P.reads(f,x);
-  requires f.requires(x);  // would be nice to be able to write P.requires(f,x)
+function Q<U,V>(f: U -> V, x : U): V
+  reads P.reads(f,x)
+  requires f.requires(x)  // would be nice to be able to write P.requires(f,x)
 {
   P(f,x)
 }
 
-function QQ(f: U -> V, x : U): V
-  reads ((() => ((()=>f)()).reads)())((()=>x)());
-  requires ((() => ((()=>f)()).requires)())((()=>x)());
+function QQ<U,V>(f: U -> V, x : U): V
+  reads ((() => ((()=>f)()).reads)())((()=>x)())
+  requires ((() => ((()=>f)()).requires)())((()=>x)())
 {
   ((() => P)())((()=>f)(),(()=>x)())
 }
-- 
cgit v1.2.3