diff options
| author |  Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-08 15:33:23 +0100 |
|---|---|---|
| committer | Nadia Polikarpova <nadia.polikarpova@gmail.com> | 2013-02-08 15:33:23 +0100 |
| commit | 6a73bfff8499eb7a128de01c20488a9f53e397c7 (patch) | |
| tree | 1958510741be38d9972453b2ad42ab265270fb43 /Test/dafny3/Dijkstra.dfy | |
| parent | bc0e2a5f6ef893c549c3a244faa17e7f235a2de0 (diff) | |
Changed calc syntax (custom operators are now written before the hint)
Diffstat (limited to 'Test/dafny3/Dijkstra.dfy')
| -rw-r--r-- | Test/dafny3/Dijkstra.dfy | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Test/dafny3/Dijkstra.dfy b/Test/dafny3/Dijkstra.dfy index d3ff244a..7497618c 100644 --- a/Test/dafny3/Dijkstra.dfy +++ b/Test/dafny3/Dijkstra.dfy @@ -28,8 +28,8 @@ ghost method lemma_ping(j: nat, n: nat) j <= n;
{ lemma_ping(j - 1, n - 1); }
j - 1 <= f(n - 1);
- { lemma_ping(j - 1, f(n - 1)); }
- ==> j - 1 <= f(f(n - 1));
+ ==> { lemma_ping(j - 1, f(n - 1)); }
+ j - 1 <= f(f(n - 1));
// (0)
j - 1 <= f(f(n - 1)) && f(f(n - 1)) < f(n);
==> j - 1 < f(n);
|