summaryrefslogtreecommitdiff
path: root/Test/dafny2/Calculations.dfy
diff options
context:
space:
mode:
Diffstat (limited to 'Test/dafny2/Calculations.dfy')
-rw-r--r--Test/dafny2/Calculations.dfy8
1 files changed, 1 insertions, 7 deletions
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy
index c48f2000..1ddd8603 100644
--- a/Test/dafny2/Calculations.dfy
+++ b/Test/dafny2/Calculations.dfy
@@ -209,10 +209,4 @@ ghost method Window(xs: List, ys: List)
length(xs) == length(ys) ==> length(reverse(xs)) == length(reverse(xs));
true;
}
-}
-
-// Empty calculations are also allowed, but they don't generate any Boogie code.
-ghost method Empty()
-{
- calc {}
-}
+} \ No newline at end of file