diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 19:01:37 +0200 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2012-09-19 19:01:37 +0200 |
| commit | a1e5529fc5f001be15a5a3b9730dbe890314581d (patch) | |
| tree | 77495d516f7855673c75af1790a5b64d45116b69 /Test/dafny2 | |
| parent | 8264fd48ce81180c78fa3f9c76ed31c52723017b (diff) | |
Allow multiple calc/block statements in a hint. Removed the empty calc test from dafny2/Calculations, as it actually belongs in dafny0.
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 8 |
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 |