diff options
| author |  rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-11-08 20:53:30 +0000 |
| commit | 17efb869d2b4a00c26e04b27de34b8bc643ad581 (patch) | |
| tree | a9368d57c7f5fe58b7a66ce08e12fe1c8e6e9912 /Test/dafny0/Simple.dfy | |
| parent | 2efa59dea051803bc716d02070aa013397cfccc4 (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>;
+}
|