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
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' ⇒
Hallo,
I've been playing around with corec and friends in combination with the
lazy lists from "$AFP/Coinductive/Coinductive_List" and encountered the
following problem:
Suppose I want a function that takes two (implicitly sorted) lazy lists
and merges them in the following fashion:
