summaryrefslogtreecommitdiff
path: root/Test/hofs/Simple.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/hofs/Simple.dfy')
-rw-r--r--Test/hofs/Simple.dfy20
1 files changed, 10 insertions, 10 deletions
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)())
}