# [isabelle-dev] Of lazy lists and friendly corecs

```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:
```
primcorec lmerge :: "int llist ⇒ int llist ⇒ int llist" where
"lmerge xs ys = (if lnull xs then ys
else if lnull ys then xs
```
else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) ys)
```                   else LCons (lhd ys) (lmerge xs (ltl ys)))"

```
I've still not fully understood what ‘friendly’ means, but I should be very surprised if this function were not friendly. So I tried this:
```
friend_of_corec lmerge where
"lmerge xs ys = (if lnull xs ∧ lnull ys then LNil
else if lnull xs then LCons (lhd ys) (ltl ys)
else if lnull ys then LCons (lhd xs) (ltl xs)
```
else if lhd xs ≤ lhd ys then LCons (lhd xs) (lmerge (ltl xs) ys)
```                   else LCons (lhd ys) (lmerge xs (ltl ys)))"

Unfortunately, I get the following error:

```
exception TYPE raised (line 168 of "consts.ML"): Illegal type for constant "Coinductive_List.llist.LNil" :: 'b
```
I now have the following questions:
```
1. Something like "if lnull xs then ys" works in primcorec, but in corec and friend_of_corec I have to do odd things like "LCons (lhd ys) (ltl ys)". Is that a known limitation? 2. What is the relationship between primcorec and friendliness? If I have a function defined by primcorec, is the additional step with friend_of_corec fundamentally necessary or is that just a technical issue? (I would have naïvely assumed that primitively-corecursive functions are always friendly or something like that)
```3. What causes the above error and how do I get around it?

Cheers,

Manuel

```
```_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
```