diff options
Diffstat (limited to 'Test/dafny1/Induction.dfy')
| -rw-r--r-- | Test/dafny1/Induction.dfy | 5 |
1 files changed, 1 insertions, 4 deletions
diff --git a/Test/dafny1/Induction.dfy b/Test/dafny1/Induction.dfy index 2c90769b..de5a3358 100644 --- a/Test/dafny1/Induction.dfy +++ b/Test/dafny1/Induction.dfy @@ -136,10 +136,7 @@ class IntegerInduction { }
}
-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<T>(tree: Tree<T>): int
|