diff options
Diffstat (limited to 'Test/dafny0/ListContents.dfy')
| -rw-r--r-- | Test/dafny0/ListContents.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny0/ListContents.dfy b/Test/dafny0/ListContents.dfy index 01d8b63b..759c6afd 100644 --- a/Test/dafny0/ListContents.dfy +++ b/Test/dafny0/ListContents.dfy @@ -77,10 +77,10 @@ class Node<T> { (forall i :: 0 <= i && i < |reverse.list| ==> old(list)[i] == reverse.list[|reverse.list|-1-i]);
{
var nx := current.next;
- assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]);
+ assert nx != null ==> (forall i :: 0 <= i && i < |nx.list| ==> current.list[1+i] == nx.list[i]); // lemma
// ..., reverse, current, nx, ...
- assert current.data == current.list[0];
+ assert current.data == current.list[0]; // lemma
current.next := reverse;
current.footprint := {current} + reverse.footprint;
current.list := [current.data] + reverse.list;
|