diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-04-27 13:30:28 -0700 |
| commit | 15cc51aab574c34a3c3302ccc1a4bdd6063cfa4b (patch) | |
| tree | 4bb849d75f9527852eb92973c04b48b90bf4f55c /Test/dafny0/Coinductive.dfy | |
| parent | dde9e3560e445addc6cbcfc5bfb219b0bc5cc79f (diff) | |
Dafny: added resolution tests cases for inductive datatypes
Diffstat (limited to 'Test/dafny0/Coinductive.dfy')
| -rw-r--r-- | Test/dafny0/Coinductive.dfy | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/Test/dafny0/Coinductive.dfy b/Test/dafny0/Coinductive.dfy index fdb8c06b..35f17c1c 100644 --- a/Test/dafny0/Coinductive.dfy +++ b/Test/dafny0/Coinductive.dfy @@ -26,6 +26,16 @@ module TestInductiveDatatypes datatype List<T> = Nil | Cons(T, List);
}
+module MoreInductive {
+ datatype Tree<G> = Node(G, List<Tree<G>>);
+ datatype List<T> = Nil | Cons(T, List<T>);
+
+ datatype M = All(List<M>);
+ datatype H<'a> = HH('a, Tree<'a>);
+ datatype K<'a> = KK('a, Tree<K<'a>>); // error
+ datatype L<'a> = LL('a, Tree<List<L<'a>>>);
+}
+
// --------------------------------------------------
module TestCoinductiveDatatypes
|