diff options
Diffstat (limited to 'Test/dafny3/SimpleCoinduction.dfy')
| -rw-r--r-- | Test/dafny3/SimpleCoinduction.dfy | 12 |
1 files changed, 10 insertions, 2 deletions
diff --git a/Test/dafny3/SimpleCoinduction.dfy b/Test/dafny3/SimpleCoinduction.dfy index 5a8ab288..cc92a6f1 100644 --- a/Test/dafny3/SimpleCoinduction.dfy +++ b/Test/dafny3/SimpleCoinduction.dfy @@ -64,7 +64,6 @@ copredicate True(s: Stream) comethod AlwaysTrue(s: Stream)
ensures True(s);
{
- AlwaysTrue(s.tail); // WHY does this not happen automatically? (Because 's' is not quantified over)
}
copredicate AlsoTrue(s: Stream)
@@ -75,7 +74,16 @@ copredicate AlsoTrue(s: Stream) comethod AlsoAlwaysTrue(s: Stream)
ensures AlsoTrue(s);
{
- // AlsoAlwaysTrue(s); // here, the recursive call is not needed, because it uses the same 's', so 's' does not need to be quantified over
+}
+
+copredicate TT(y: int)
+{
+ TT(y+1)
+}
+
+comethod AlwaysTT(y: int)
+ ensures TT(y);
+{
}
// -----------------------------------------------------------------------
|