Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax

1 files changed, 2 insertions, 5 deletions

diff --git a/Test/dafny1/SchorrWaite.dfy b/Test/dafny1/SchorrWaite.dfy
index 95cdab89..8da32b05 100644
--- a/Test/dafny1/SchorrWaite.dfy
+++ b/Test/dafny1/SchorrWaite.dfy
@@ -10,6 +10,8 @@ class Node {
   ghost var pathFromRoot: Path;

 }

 

+datatype Path = Empty | Extend(Path, Node);

+

 class Main {

   method RecursiveMark(root: Node, ghost S: set<Node>)

     requires root in S;

@@ -265,8 +267,3 @@ class Main {
     }

   }

 }

-

-datatype Path {

-  Empty;

-  Extend(Path, Node);

-}