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

1 files changed, 10 insertions, 21 deletions

diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy
index 21f0dda8..9df11a67 100644
--- a/Test/dafny0/TypeTests.dfy
+++ b/Test/dafny0/TypeTests.dfy
@@ -13,37 +13,26 @@ class C {
   }

 }

 

-datatype D {

-  A;

-}

-

-datatype Nothing {  // error: no grounding constructor

-}

+datatype D = A;

 

-datatype NeverendingList {  // error: no grounding constructor

-  Cons(int, NeverendingList);

-}

+datatype NeverendingList = Cons(int, NeverendingList);  // error: no grounding constructor

 

-datatype MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(TheCounterpart<T>, C);

-}

 

-datatype TheCounterpart<T> {

-  TreeLike(TheCounterpart<T>, TheCounterpart<T>);

+datatype TheCounterpart<T> =

+  TreeLike(TheCounterpart<T>, TheCounterpart<T>) |

   More(MutuallyRecursiveDataType<T>);

-}

 

 // these 'ReverseOrder_' order tests may be called white-box unit tests

-datatype ReverseOrder_MutuallyRecursiveDataType<T> {

-  FromANumber(int);  // this is the base case

+datatype ReverseOrder_MutuallyRecursiveDataType<T> =

+  FromANumber(int) |  // this is the base case

   Else(ReverseOrder_TheCounterpart<T>, C);

-}

 

-datatype ReverseOrder_TheCounterpart<T> {

-  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>);

+datatype ReverseOrder_TheCounterpart<T> =

+  TreeLike(ReverseOrder_TheCounterpart<T>, ReverseOrder_TheCounterpart<T>) |

   More(ReverseOrder_MutuallyRecursiveDataType<T>);

-}

 

 // ---------------------