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/dafny1/Rippling.dfy | |
| parent | e1bf8c0bfff274a0651fb581951cfcaae8b34007 (diff) | |
Dafny: permanently changed the syntax of "datatype" declarations to what previously was an alternative syntax
Diffstat (limited to 'Test/dafny1/Rippling.dfy')
| -rw-r--r-- | Test/dafny1/Rippling.dfy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny1/Rippling.dfy b/Test/dafny1/Rippling.dfy index 3a455077..fdce6dc7 100644 --- a/Test/dafny1/Rippling.dfy +++ b/Test/dafny1/Rippling.dfy @@ -1,16 +1,16 @@ // Datatypes
-datatype Bool { False; True; }
+datatype Bool = False | True;
-datatype Nat { Zero; Suc(Nat); }
+datatype Nat = Zero | Suc(Nat);
-datatype List { Nil; Cons(Nat, List); }
+datatype List = Nil | Cons(Nat, List);
-datatype Pair { Pair(Nat, Nat); }
+datatype Pair = Pair(Nat, Nat);
-datatype PList { PNil; PCons(Pair, PList); }
+datatype PList = PNil | PCons(Pair, PList);
-datatype Tree { Leaf; Node(Tree, Nat, Tree); }
+datatype Tree = Leaf | Node(Tree, Nat, Tree);
// Boolean functions
|