Zulip Chat Archive

Stream: general

Topic: Inductive structures?


view this post on Zulip Mario Carneiro (Jan 25 2021 at 20:05):

yes, it is impossible. Structures are by definition non-recursive inductive types with one constructor

view this post on Zulip James Kay (Jan 25 2021 at 20:08):

Oh, thank you :(

view this post on Zulip James Kay (Jan 25 2021 at 20:25):

Is there any equivalent syntax for recursive definitions to allow order-independent projection/construction, so I don't have to update all my code whenever I add or re-order a field?

view this post on Zulip Eric Wieser (Jan 25 2021 at 20:50):

If you define the projections immediately, then you only have to adjust for the field order in those places


Last updated: May 12 2021 at 23:13 UTC