Changed calc syntax (custom operators are now written before the hint)

2 files changed, 4 insertions, 4 deletions

diff --git a/Test/dafny3/CalcExample.dfy b/Test/dafny3/CalcExample.dfy
index c94c18d2..dcd41077 100644
--- a/Test/dafny3/CalcExample.dfy
+++ b/Test/dafny3/CalcExample.dfy
@@ -19,8 +19,8 @@ method M(a: int, b: int, c: int, x: int)
     f(f(a, b), c);

     { assert f(a, b) == x; }

     f(x, c);

-    { assert c <= x; Monotonicity(c, x); }

-    <= f(x, x);

+    <= { assert c <= x; Monotonicity(c, x); }

+    f(x, x);

     { DiagonalIdentity(x); }

     x;

   }

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);