1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
Coinductive.dfy(13,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'Rec_Forever' can be constructed
Coinductive.dfy(16,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'D' can be constructed
Coinductive.dfy(38,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'K' can be constructed
Coinductive.dfy(64,11): Error: because of cyclic dependencies among constructor argument types, no instances of datatype 'NotFiniteEnough_Dt' can be constructed
Coinductive.dfy(93,8): Error: a copredicate can be called recursively only in positive positions
Coinductive.dfy(94,8): Error: a copredicate can be called recursively only in positive positions
Coinductive.dfy(95,8): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(95,21): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(101,5): Error: a copredicate can be called recursively only in positive positions
Coinductive.dfy(104,27): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(105,28): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(106,17): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
Coinductive.dfy(116,24): Error: a copredicate can be called recursively only in positive positions and cannot sit inside an unbounded existential quantifier
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
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(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
|
