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

1 files changed, 5 insertions, 17 deletions

diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy
index f363a023..a94283e6 100644
--- a/Test/dafny1/TreeDatatype.dfy
+++ b/Test/dafny1/TreeDatatype.dfy
@@ -1,13 +1,8 @@
 // ------------------ generic list, non-generic tree

 

-datatype List<T> {

-  Nil;

-  Cons(T, List<T>);

-}

+datatype List<T> = Nil | Cons(T, List<T>);

 

-datatype Tree {

-  Node(int, List<Tree>);

-}

+datatype Tree = Node(int, List<Tree>);

 

 static function Inc(t: Tree): Tree

 {

@@ -24,9 +19,7 @@ static function ForestInc(forest: List<Tree>): List<Tree>
 

 // ------------------ generic list, generic tree (but GInc defined only for GTree<int>

 

-datatype GTree<T> {

-  Node(T, List<GTree<T>>);

-}

+datatype GTree<T> = Node(T, List<GTree<T>>);

 

 static function GInc(t: GTree<int>): GTree<int>

 {

@@ -43,14 +36,9 @@ static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
 

 // ------------------ non-generic structures

 

-datatype TreeList {

-  Nil;

-  Cons(OneTree, TreeList);

-}

+datatype TreeList = Nil | Cons(OneTree, TreeList);

 

-datatype OneTree {

-  Node(int, TreeList);

-}

+datatype OneTree = Node(int, TreeList);

 

 static function XInc(t: OneTree): OneTree

 {