diff options
Diffstat (limited to 'Test/dafny1/TreeDatatype.dfy')
| -rw-r--r-- | Test/dafny1/TreeDatatype.dfy | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/Test/dafny1/TreeDatatype.dfy b/Test/dafny1/TreeDatatype.dfy index 763cef1b..beb1597e 100644 --- a/Test/dafny1/TreeDatatype.dfy +++ b/Test/dafny1/TreeDatatype.dfy @@ -7,13 +7,13 @@ datatype List<T> = Nil | Cons(T, List<T>); datatype Tree = Node(int, List<Tree>);
-static function Inc(t: Tree): Tree
+function Inc(t: Tree): Tree
{
match t
case Node(n, children) => Tree.Node(n+1, ForestInc(children))
}
-static function ForestInc(forest: List<Tree>): List<Tree>
+function ForestInc(forest: List<Tree>): List<Tree>
{
match forest
case Nil => forest
@@ -24,13 +24,13 @@ static function ForestInc(forest: List<Tree>): List<Tree> datatype GTree<T> = Node(T, List<GTree<T>>);
-static function GInc(t: GTree<int>): GTree<int>
+function GInc(t: GTree<int>): GTree<int>
{
match t
case Node(n, children) => GTree.Node(n+1, GForestInc(children))
}
-static function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
+function GForestInc(forest: List<GTree<int>>): List<GTree<int>>
{
match forest
case Nil => forest
@@ -43,13 +43,13 @@ datatype TreeList = Nil | Cons(OneTree, TreeList); datatype OneTree = Node(int, TreeList);
-static function XInc(t: OneTree): OneTree
+function XInc(t: OneTree): OneTree
{
match t
case Node(n, children) => OneTree.Node(n+1, XForestInc(children))
}
-static function XForestInc(forest: TreeList): TreeList
+function XForestInc(forest: TreeList): TreeList
{
match forest
case Nil => forest
|