CoResolution.dfy(18,11): Error: member Undeclared# does not exist in class TestClass CoResolution.dfy(19,6): Error: unresolved identifier: Undeclared# CoResolution.dfy(22,9): Error: unresolved identifier: _k CoResolution.dfy(41,8): Error: == can only be applied to expressions of types that support equality (got Stream<_T0>) CoResolution.dfy(52,8): Error: Assignment to non-ghost variable is not allowed in this context (because this is a ghost method or because the statement is guarded by a specification-only expression) CoResolution.dfy(70,12): Error: a copredicate is not allowed to declare any reads clause CoResolution.dfy(76,33): Error: a copredicate is not allowed to declare any ensures clause CoResolution.dfy(86,20): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(90,20): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(99,5): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(113,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(114,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(119,24): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(125,28): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(133,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(134,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(139,26): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(145,30): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(153,4): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(155,4): Error: a recursive call from a copredicate can go only to other copredicates CoResolution.dfy(171,13): Error: a recursive call from a colemma can go only to other colemmas and prefix lemmas CoResolution.dfy(206,12): Error: type variable '_T0' in the function call to 'A' could not be determined CoResolution.dfy(206,13): Error: the type of this expression is underspecified CoResolution.dfy(206,19): Error: type variable '_T0' in the function call to 'S' could not be determined 24 resolution/type errors detected in CoResolution.dfy