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

1 files changed, 5 insertions, 12 deletions

diff --git a/Test/dafny0/TypeAntecedents.dfy b/Test/dafny0/TypeAntecedents.dfy
index 38050b88..2bedd37d 100644
--- a/Test/dafny0/TypeAntecedents.dfy
+++ b/Test/dafny0/TypeAntecedents.dfy
@@ -1,10 +1,8 @@
 // -------- This is an example of what was once logically (although not trigger-ly) unsound ---

 

-datatype Wrapper<T> {

-  Wrap(T);

-}

-datatype Unit { It; }

-datatype Color { Yellow; Blue; }

+datatype Wrapper<T> = Wrap(T);

+datatype Unit = It;

+datatype Color = Yellow | Blue;

 

 function F(a: Wrapper<Unit>): bool

   ensures a == Wrapper.Wrap(Unit.It);

@@ -49,10 +47,7 @@ class MyClass {
   function H(): int { 5 }

 }

 

-datatype List {

-  Nil;

-  Cons(MyClass, List);

-}

+datatype List =  Nil | Cons(MyClass, List);

 

 method M(list: List, S: set<MyClass>) returns (ret: int)

   modifies S;

@@ -97,8 +92,6 @@ function NF(): MyClass;
 

 function TakesADatatype(a: List): int { 12 }

 

-datatype GenData<T> {

-  Pair(T, T);

-}

+datatype GenData<T> = Pair(T, T);

 

 function AlsoTakesADatatype<U>(p: GenData<U>): int { 17 }