blob: cab2524a0f061cac2d5e93d8bf324d908f220f3c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
// RUN: %dafny "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
lemma T(a: int) returns (b: int)
ensures a == b
{
calc {
a;
}
}
lemma A(i: int)
ensures false
{
if * {
} else {
}
}
|