diff options
| author |  Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 15:39:52 -0700 |
|---|---|---|
| committer | Unknown <leino@LEINO6.redmond.corp.microsoft.com> | 2012-06-22 15:39:52 -0700 |
| commit | 2d63e53e2590303ed833b6552f8a2d383176958a (patch) | |
| tree | 0330401ddc0e927bcd23d5cff106a20f88f582c1 /Test/dafny0/TypeTests.dfy | |
| parent | 7c6cfaa37c96349fda99823c6f98a576dba194b4 (diff) | |
Dafny: deal with equality-support issues in refinements
Dafny: a small amount of refactoring and bug fixes
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>
|