diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-10-04 16:39:13 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-10-04 16:39:13 -0700 |
| commit | 5441447b52d9850683679c1dc7aa675d8ddc2927 (patch) | |
| tree | c9172fbf1853fe13c2d42da1d8d9987d16025283 /Test/dafny0/Corecursion.dfy | |
| parent | a54b7d394f92a9af32cff46e854eb4d37705439e (diff) | |
changed default decreases clause for functions with a reads clause: use the reads clause followed by the list of parameters
Diffstat (limited to 'Test/dafny0/Corecursion.dfy')
| -rw-r--r-- | Test/dafny0/Corecursion.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/dafny0/Corecursion.dfy b/Test/dafny0/Corecursion.dfy index 9f1b1328..0918d6f5 100644 --- a/Test/dafny0/Corecursion.dfy +++ b/Test/dafny0/Corecursion.dfy @@ -9,7 +9,7 @@ module CoRecursion { More(n, AscendingChain(n+1))
}
- function AscendingChainAndRead(n: int): Stream<int>
+ function AscendingChainAndRead(n: nat): Stream<int>
reads this; // with a reads clause, this function is not a co-recusvie function
{
More(n, AscendingChainAndRead(n+1)) // error: cannot prove termination
|