Test/hofs/Apply.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29

// RUN: %dafny /print:"%t.print" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"


method Apply(x : int) returns (i : int)
  ensures i == x;
{
  i := (x => x)(x);
}

function method Const<A,B>(a : A) : B -> A {
  b => a
}

method Test(m : map<int, int -> int -> int>)
{
  assume forall i :: i in m;
  assume forall i, x :: m[i].requires(x);
  assume forall i, x, y :: m[i](x).requires(y);
  assume m[1](2)(3) > 5;
  assert ((m[1])(2))(3) > 4;
}

method Main() {
  assert forall x : int, y : int :: Const(x)(y) == (Const(x))(y);
  assert (a => b => a) == (u : int) => (v : int) => u;
  assert Const == (u : int) => (v : int) => u;
}