Hi Manuel,
I've played around a bit with lmerge. It magically works if you replace the selectors with
case statements (in Isabelle/5c2c559f01eb):
friend_of_corec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
"lmerge xs ys =
(case xs of LNil ⇒ (case ys of LNil ⇒ LNil | LCons y ys' ⇒
Hi Manuel,
a function is friendly if it produces at least one constructor after applying at most one
constructor to the codatatype argument. This does not have anything to do with primitive
corecursion, because the codatatype result type need not be a argument type---and even if
it is, there
