diff options
Diffstat (limited to 'Test/dafny0/TypeTests.dfy')
| -rw-r--r-- | Test/dafny0/TypeTests.dfy | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Test/dafny0/TypeTests.dfy b/Test/dafny0/TypeTests.dfy index 8434f06c..2dea7a52 100644 --- a/Test/dafny0/TypeTests.dfy +++ b/Test/dafny0/TypeTests.dfy @@ -86,7 +86,8 @@ method ArrayRangeAssignments(a: array<C>, c: C) // --------------------- tests of restrictions on subranges (nat)
-method K(s: set<nat>) { // error: not allowed to instantiate 'set' with 'nat'
+method K() {
+ var s: set<nat>; // error: not allowed to instantiate 'set' with 'nat'
var d: MutuallyRecursiveDataType<nat>; // error: not allowed to instantiate with 'nat'
var a := new nat[100]; // error: not allowed the type array<nat>
var b := new nat[100,200]; // error: not allowed the type array2<nat>
|