summaryrefslogtreecommitdiff
path: root/Test/dafny1/pow2.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny1/pow2.dfy')
-rw-r--r--Test/dafny1/pow2.dfy8
1 files changed, 4 insertions, 4 deletions
diff --git a/Test/dafny1/pow2.dfy b/Test/dafny1/pow2.dfy
index 52cddaac..c7e4bc63 100644
--- a/Test/dafny1/pow2.dfy
+++ b/Test/dafny1/pow2.dfy
@@ -36,7 +36,7 @@ ghost method Lemma(n: int)
ensures pow2_slow(n) == Square(pow2_slow(n/2));
{
if (n != 0) {
- call Lemma(n-2);
+ Lemma(n-2);
}
}
@@ -46,9 +46,9 @@ ghost method Theorem(n: int)
{
if (n == 0) {
} else if (IsEven(n)) {
- call Lemma(n);
- call Theorem(n/2);
+ Lemma(n);
+ Theorem(n/2);
} else {
- call Theorem(n-1);
+ Theorem(n-1);
}
}