diff options
| author |  Rustan Leino <leino@microsoft.com> | 2011-05-11 17:25:34 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2011-05-11 17:25:34 -0700 |
| commit | 27241e69516368f116baea922938d1cb10570d85 (patch) | |
| tree | c4079369967b34e88de4b3921b3710b605baa18a /Test/dafny0/NatTypes.dfy | |
| parent | dcaef29ffbe2570632e7368d27377fb9ac282d7b (diff) | |
Dafny:
* added missing error checking for ghost-vs-physical contexts (e.g., use of the "old" keyword)
* check that arrays are not null when accessed
* added dafny1/FindZero.dfy test case
Diffstat (limited to 'Test/dafny0/NatTypes.dfy')
| -rw-r--r-- | Test/dafny0/NatTypes.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/NatTypes.dfy b/Test/dafny0/NatTypes.dfy index 93bd4b65..6b7ce9b9 100644 --- a/Test/dafny0/NatTypes.dfy +++ b/Test/dafny0/NatTypes.dfy @@ -60,7 +60,7 @@ datatype List<T> { Cons(nat, T, List<T>);
}
-method MatchIt(list: List<bool>) returns (k: nat)
+method MatchIt(list: List<object>) returns (k: nat)
{
match (list) {
case Nil =>
|