Stream: Coq users

Topic: ✔ Mutual coinduction

view this post on Zulip 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.

view this post on Zulip Notification Bot (Jul 19 2023 at 14:45):

maxv has marked this topic as resolved.

view this post on Zulip 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: Jun 13 2024 at 21:01 UTC