Test/hofs/Renaming.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

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

function OnId(f : (bool -> bool) -> int) : int
  reads f.reads(x => x);
  requires f.requires(y => y);
{
  f(z => z)
}

method Equal() {
  var id1 : bool -> bool := x => x;
  var id2                := y => y;
  assert forall x :: id1(x) == id2(x);
  assert id1 == id2;
}

method K<A,B>(P : (A -> A) -> bool)
{
  assume P.requires(x => x);
  assume P(y => y);
  assert P(z => z);
  assert (x => y => x) == ((a : A) => (b : B) => a);
}