From 172554c51fad4092f2b4e52a921ad0e86fa67ca6 Mon Sep 17 00:00:00 2001 From: Rustan Leino Date: Wed, 6 Mar 2013 15:09:04 -0800 Subject: Renamed "parallel" statement to "forall" statement, and made the parentheses around the bound variables optional. --- Test/dafny2/Calculations.dfy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'Test/dafny2') 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(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); -- cgit v1.2.3