diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-14 00:08:52 +0100 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-14 00:08:52 +0100 |
| commit | 51cdc2fc3c57ecb20df351960e3048fdf51b5628 (patch) | |
| tree | f40e80d626a78d2498e5b8c0580e42c9c3c2aba4 /Test/dafny2 | |
| parent | 29aa0357017c1d23deedbf18995a6863e11ac07d (diff) | |
| parent | 2c74f9200db870814ea3dae63484cbe969ec3526 (diff) | |
Merge
Diffstat (limited to 'Test/dafny2')
| -rw-r--r-- | Test/dafny2/Calculations.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny2/Calculations.dfy b/Test/dafny2/Calculations.dfy index 19e0645f..777be464 100644 --- a/Test/dafny2/Calculations.dfy +++ b/Test/dafny2/Calculations.dfy @@ -121,7 +121,7 @@ ghost method Lemma_Revacc(xs: List, ys: List) assert concat(revacc(xrest, Cons(x, Nil)), ys)
== revacc(xrest, concat(Cons(x, Nil), ys));
- assert forall g, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
+ assert forall g: _T0, gs :: concat(Cons(g, Nil), gs) == Cons(g, gs);
assert revacc(xrest, concat(Cons(x, Nil), ys))
== // the assert lemma just above
|