Zulip Chat Archive

Stream: general

Topic: Inductive structures?

Mario Carneiro (Jan 25 2021 at 20:05):

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

James Kay (Jan 25 2021 at 20:08):

Oh, thank you :(

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?

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: Dec 20 2023 at 11:08 UTC