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

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

diff --git a/Test/hofs/Examples.dfy b/Test/hofs/Examples.dfy
index be2672f5..306d278d 100644
--- a/Test/hofs/Examples.dfy
+++ b/Test/hofs/Examples.dfy
@@ -1,14 +1,14 @@
 // RUN: %dafny /print:"%t.print" "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
-function Apply(f: A -> B, x: A): B
+function Apply<A,B>(f: A -> B, x: A): B
   reads f.reads(x);
   requires f.requires(x);
 {
   f(x)
 }
 
-function Apply'(f: A -> B) : A -> B
+function Apply'<A,B>(f: A -> B) : A -> B
 {
   x reads f.reads(x)
     requires f.requires(x)
@@ -16,7 +16,7 @@ function Apply'(f: A -> B) : A -> B
 }
 
 
-function Compose(f: B -> C, g:A -> B): A -> C
+function Compose<A,B,C>(f: B -> C, g:A -> B): A -> C
 {
   x reads g.reads(x)
     reads if g.requires(x) then f.reads(g(x)) else {}
@@ -25,21 +25,21 @@ function Compose(f: B -> C, g:A -> B): A -> C
     => f(g(x))
 }
 
-function W(f : (A,A) -> A): A -> A
+function W<A>(f : (A,A) -> A): A -> A
 {
   x requires f.requires(x,x)
     reads f.reads(x,x)
     => f(x,x)
 }
 
-function Curry(f : (A,B) -> C) : A -> B -> C
+function Curry<A,B,C>(f : (A,B) -> C) : A -> B -> C
 {
   x => y requires f.requires(x,y)
          reads f.reads(x,y)
          => f(x,y)
 }
 
-function Uncurry(f : A -> B -> C) : (A,B) -> C
+function Uncurry<A,B,C>(f : A -> B -> C) : (A,B) -> C
 {
   (x,y) requires f.requires(x)
         requires f(x).requires(y)
@@ -48,7 +48,7 @@ function Uncurry(f : A -> B -> C) : (A,B) -> C
         => f(x)(y)
 }
 
-function S(f : (A,B) -> C, g : A -> B): A -> C
+function S<A,B,C>(f : (A,B) -> C, g : A -> B): A -> C
 {
   x requires g.requires(x)
     requires f.requires(x,g(x))
-- 
cgit v1.2.3