blob: d03d7c796e85ed6d7dfde050ec1544d6e7724b2d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
// RUN: %dafny /compile:0 /print:"%t.print" /dprint:"%t.dprint" "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
function KeepDoin'It(x: nat): nat
{
KeepDoin'ItToo(x + 1)
}
function KeepDoin'ItToo(x: nat): nat
{
KeepDoin'It(x + 1)
}
lemma Test(r: nat)
{
assert KeepDoin'It(20) == r;
}
|
