diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-27 01:44:26 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-27 01:44:26 -0700 |
| commit | 803f42612314d2d27f20dfa476bf0ff8ed24d958 (patch) | |
| tree | f341d7239381047f31d761938df3b9e1f7a3874c /Test/dafny0/Simple.dfy | |
| parent | e1bf8c0bfff274a0651fb581951cfcaae8b34007 (diff) | |
Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 12 |
1 files changed, 4 insertions, 8 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index e1416094..ac3a4792 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -39,16 +39,12 @@ class MyClass<T,U> { // some datatype stuff:
-datatype List<T> {
- Nil;
- Cons(T, List<T>);
-}
+datatype List<T> = Nil | Cons(T, List<T>);
-datatype WildData {
- Something();
- JustAboutAnything(bool, myName: set<int>, int, WildData);
+datatype WildData =
+ Something() |
+ JustAboutAnything(bool, myName: set<int>, int, WildData) |
More(List<int>);
-}
class C {
var w: WildData;
|