diff options
author | 2011-05-27 01:44:26 -0700 | |
---|---|---|
committer | 2011-05-27 01:44:26 -0700 | |
commit | 065fa79887779fbfbc14700744acd684c59aa3ec (patch) | |
tree | bfa784eeee8bbea39c3820b5cf5c0cf1022f0fec /Test/dafny0/DTypes.dfy | |
parent | 9a714cafa2e4d6551f28c57187c28333cc155527 (diff) |
Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax
Diffstat (limited to 'Test/dafny0/DTypes.dfy')
-rw-r--r-- | Test/dafny0/DTypes.dfy | 10 |
1 files changed, 2 insertions, 8 deletions
diff --git a/Test/dafny0/DTypes.dfy b/Test/dafny0/DTypes.dfy index b402c335..55d107c5 100644 --- a/Test/dafny0/DTypes.dfy +++ b/Test/dafny0/DTypes.dfy @@ -74,10 +74,7 @@ class Node { } class CP<T,U> {
}
-datatype Data {
- Lemon;
- Kiwi(int);
-}
+datatype Data = Lemon | Kiwi(int);
function G(d: Data): int
requires d != Data.Lemon;
@@ -89,10 +86,7 @@ function G(d: Data): int // -------- some things about induction ---------------------------------
-datatype Tree<T> {
- Leaf(T);
- Branch(Tree<T>, Tree<T>);
-}
+datatype Tree<T> = Leaf(T) | Branch(Tree<T>, Tree<T>);
class DatatypeInduction<T> {
function LeafCount<G>(tree: Tree<G>): int
|