diff options
Diffstat (limited to 'Test/dafny2')
-rw-r--r-- | Test/dafny2/Calculations.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 79803f35..bbfab50d 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -209,7 +209,7 @@ ghost method Window(xs: List, ys: List) }
}
-// In the following we use a combination of calc and parallel
+// In the following we use a combination of calc and forall
function ith<a>(xs: List, i: nat): a
requires i < length(xs);
@@ -253,7 +253,7 @@ ghost method lemma_extensionality(xs: List, ys: List) }
Cons(y, xrest);
{
- parallel (j: nat | j < length(xrest)) {
+ forall (j: nat | j < length(xrest)) {
calc {
ith(xrest, j);
ith(xs, j + 1);
|