diff options
| author |  leino <unknown> | 2014-10-28 17:44:39 -0700 |
|---|---|---|
| committer | leino <unknown> | 2014-10-28 17:44:39 -0700 |
| commit | 655b8311917e38cc2b359bad46def21de7852508 (patch) | |
| tree | 8c7881bac939013d25a28e82e9860c456f034ea0 /Test/dafny0/TypeParameters.dfy | |
| parent | 6c9a50e81dbdb791c558ac0a3463f01ee6a7f580 (diff) | |
Disallow automatic completion of type arguments to the LHS of datatype declarations
Diffstat (limited to 'Test/dafny0/TypeParameters.dfy')
| -rw-r--r-- | Test/dafny0/TypeParameters.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/TypeParameters.dfy b/Test/dafny0/TypeParameters.dfy index 900b6110..aa3d7671 100644 --- a/Test/dafny0/TypeParameters.dfy +++ b/Test/dafny0/TypeParameters.dfy @@ -335,7 +335,7 @@ module ArrayTypeMagic { return b[..];
}
- datatype ArrayCubeTree = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
+ datatype ArrayCubeTree<T> = Leaf(array3) | Node(ArrayCubeTree, ArrayCubeTree)
datatype AnotherACT<T> = Leaf(array3) | Node(AnotherACT, AnotherACT)
datatype OneMoreACT<T,U> = Leaf(array3) | Node(OneMoreACT, OneMoreACT)
|