Stream: Coq users

Topic: ✔ What is the difference between ind-ind and mut-ind


view this post on Zulip Théo Winterhalter (Apr 12 2023 at 08:12):

With mutual inductive types you can only refer to the other inductive types, but with inductive inductive types you can also refer to the constructors.

view this post on Zulip Notification Bot (Apr 12 2023 at 08:26):

walker has marked this topic as resolved.

view this post on Zulip Notification Bot (Apr 12 2023 at 08:26):

walker has marked this topic as unresolved.

view this post on Zulip Notification Bot (Apr 12 2023 at 08:27):

walker has marked this topic as resolved.


Last updated: Jun 24 2024 at 00:02 UTC