diff options
| author |  rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
| commit | fdef447cce5bdc57851cad1427f2a8e7cd7df35f (patch) | |
| tree | 0ba65512e599e44cb883d027a945375994bdc975 /Test/dafny0/Simple.dfy | |
| parent | c9c423ce3bde91f736266f8c9ae883b9e44acc70 (diff) | |
Start (some parsing and resolution) of adding algebraic datatypes to Dafny.
Included VSI-Benchmarks in standard tests.
Diffstat (limited to 'Test/dafny0/Simple.dfy')
| -rw-r--r-- | Test/dafny0/Simple.dfy | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/Test/dafny0/Simple.dfy b/Test/dafny0/Simple.dfy index 5f0bee87..a224ed91 100644 --- a/Test/dafny0/Simple.dfy +++ b/Test/dafny0/Simple.dfy @@ -28,3 +28,24 @@ class MyClass<T,U> { }
}
}
+
+// some datatype stuff:
+
+datatype List<T> {
+ Nil;
+ Cons(T, List<T>);
+}
+
+datatype WildData {
+ Something();
+ JustAboutAnything<G,H>(G, myName: set<H>, int, WildData);
+ More(List<int>);
+}
+
+datatype Nothing {
+}
+
+class C {
+ var w: WildData;
+ var list: List<bool>;
+}
|