Added "inductive lemma" methods

1 files changed, 10 insertions, 9 deletions

diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect
index 0ab15059..4821a0e3 100644
--- a/Test/dafny0/Coinductive.dfy.expect
+++ b/Test/dafny0/Coinductive.dfy.expect
@@ -19,12 +19,13 @@ Coinductive.dfy(205,8): Error: an inductive predicate can be called recursively
 Coinductive.dfy(206,8): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

 Coinductive.dfy(206,21): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

 Coinductive.dfy(219,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier

-Coinductive.dfy(225,5): Error: an inductive predicate can be called recursively only in positive positions

-Coinductive.dfy(228,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(229,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(230,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(240,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(246,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(247,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

-Coinductive.dfy(267,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates

-29 resolution/type errors detected in Coinductive.dfy

+Coinductive.dfy(226,16): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(238,5): Error: an inductive predicate can be called recursively only in positive positions

+Coinductive.dfy(241,28): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(242,29): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(243,17): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(253,12): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(259,15): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(260,10): Error: an inductive predicate can be called recursively only in positive positions and cannot sit inside an unbounded universal quantifier

+Coinductive.dfy(280,21): Error: a recursive call from an inductive predicate can go only to other inductive predicates

+30 resolution/type errors detected in Coinductive.dfy