diff options
| author |  leino <unknown> | 2015-05-06 17:58:00 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-05-06 17:58:00 -0700 |
| commit | f98a30f1ad7c441d8ef9e6e5740752723a43413a (patch) | |
| tree | d3be16d38a2de15865b4b25c38b8c07e41ec1173 /Test/dafny0/Coinductive.dfy.expect | |
| parent | 20f97304dda7dca7259514ca472c3c1b76262013 (diff) | |
Added inductive predicates
Diffstat (limited to 'Test/dafny0/Coinductive.dfy.expect')
| -rw-r--r-- | Test/dafny0/Coinductive.dfy.expect | 15 |
1 files changed, 14 insertions, 1 deletions
diff --git a/Test/dafny0/Coinductive.dfy.expect b/Test/dafny0/Coinductive.dfy.expect index 26fec211..0ab15059 100644 --- a/Test/dafny0/Coinductive.dfy.expect +++ b/Test/dafny0/Coinductive.dfy.expect @@ -14,4 +14,17 @@ Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in Coinductive.dfy(122,15): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(123,10): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(148,21): Error: a recursive call from a copredicate can go only to other copredicates
-16 resolution/type errors detected in Coinductive.dfy
+Coinductive.dfy(204,8): Error: an inductive predicate can be called recursively only in positive positions
+Coinductive.dfy(205,8): Error: an inductive predicate can be called recursively only in positive positions
+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
|