Hm, you may be right. I though that was going to violate: > Each recursive function call must be on a syntactic subcomponent of its formal parameter. But it

Hm, you may be right. I though that was going to violate: > Each recursive function call must be on a syntactic subcomponent of its formal parameter. But it doesn't. But you can't actually use that to get a nonterminating program, because you can't recurse over it: > Ordinary recursion is not legal over codata, because it might not terminate.