blob: 0c971e82397045c153121529a4acb8644f32451a (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
// RUN: %dafny /compile:0 /autoTriggers:1 "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
lemma lemma_ensures(x:int, RefineInt:int->int)
requires forall y :: RefineInt.requires(y);
ensures forall y :: RefineInt(y) + x == RefineInt(x) + y;
function Identity(z:int) : int
lemma test()
{
var v,w:int;
lemma_ensures(w, Identity);
//var RefineInt := Identity;
//assert RefineInt(v) == Identity(v);
assert Identity(v) + w == Identity(w) + v;
}
|