diff options
Diffstat (limited to 'Test/dafny0/Answer')
| -rw-r--r-- | Test/dafny0/Answer | 17 |
1 files changed, 12 insertions, 5 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index b462465d..7e5baa4b 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -1195,11 +1195,18 @@ Coinductive.dfy(10,11): Error: because of cyclic dependencies among constructor Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
Coinductive.dfy(35,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
Coinductive.dfy(61,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
-Coinductive.dfy(90,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(91,8): Error: a recursive copredicate call can only be done in positive positions
-Coinductive.dfy(92,8): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier
-Coinductive.dfy(92,21): Error: a recursive copredicate call can only be done in positive positions and cannot sit inside an existential quantifier
-8 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(90,8): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(91,8): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(92,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(92,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(98,5): Error: a copredicate can be called recursively only in positive positions
+Coinductive.dfy(101,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(102,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(103,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(113,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(119,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+Coinductive.dfy(120,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
+15 resolution/type errors detected in Coinductive.dfy
-------------------- Corecursion.dfy --------------------
Corecursion.dfy(15,13): Error: cannot prove termination; try supplying a decreases clause (note that only functions without side effects can be called co-recursively)
|