From ef2e49fe3617331acb73e5fe10a2da2bc3e8a02d Mon Sep 17 00:00:00 2001 From: Nadia Polikarpova Date: Sun, 23 Sep 2012 14:13:34 +0200 Subject: Use expression splitting for checking calculation steps --- Test/dafny2/Calculations.dfy | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) (limited to 'Test/dafny2') diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 1ddd8603..8c13457b 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -80,10 +80,7 @@ ghost method Lemma_Revacc_calc(xs: List, ys: List) concat(revacc(xrest, Cons(x, Nil)), ys); { Lemma_RevCatCommute(); } // forall xs,ys,zs :: revacc(xs, concat(ys, zs)) == concat(revacc(xs, ys), zs) revacc(xrest, concat(Cons(x, Nil), ys)); - { - assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs); - assert concat(Cons(x, Nil), ys) == Cons(x, ys); - } + // def. concat (x2) revacc(xrest, Cons(x, ys)); // def. revacc revacc(xs, ys); -- cgit v1.2.3