maxv (Jul 19 2023 at 14:44): maxv (Jul 19 2023 at 14:44):That's a very surprising solution. It even works in the more complicated example I had in mind, although it does mean that I have to write some code twice. Thanks a lot.
Notification Bot (Jul 19 2023 at 14:45):maxv has marked this topic as resolved.
Yann Leray (Jul 19 2023 at 16:43):Had Stream and InfinitaryTree been mutually defined, this cofixpoint definition would have worked. In your example, Stream is a nested coinductive in InfinitaryTree
Last updated: Oct 13 2024 at 01:02 UTC