Arthur Azevedo de Amorim (Nov 23 2020 at 22:58): Arthur Azevedo de Amorim (Nov 23 2020 at 22:58):Is there any plan to add support for mutually inductive types soon? I wanted to add them to my deriving library, and was considering using ELPI for writing the reification code.
Enrico Tassi (Nov 24 2020 at 06:48):Not for 8.13. I almost have universe polymorphism, but nothing for mutual fix/inductive. I guess you will have to use something else if you need it soon.
Arthur Azevedo de Amorim (Nov 24 2020 at 15:43):Got it. I'll use something else for now, but I am looking forward to doing the switch to ELPI in the future!
Enrico Tassi (Nov 24 2020 at 15:55):I'm just curious, which are the inductives you want to derive? I mean, mutual inductives are common in, say, semantics but you don't need an eqType on these (usually).
Arthur Azevedo de Amorim (Nov 25 2020 at 13:57):The first time I needed one was precisely to formalize a language (https://github.com/arthuraa/netter/blob/master/coq/Expr.v). It would have been possible to do without the power of eq, but having it readily available is pretty convenient (e.g. sometimes it is better to write e1 == e2 than doing a complicated match).
Enrico Tassi (Nov 25 2020 at 14:03):disentangling zexpr and qexpr is a bit painful, but it seems easy to parametrize the two over bexpr. Then bexpr can be non mutual (assuming you need == there)
Enrico Tassi (Nov 25 2020 at 14:06):Said otherwise, the encoding, at least in this case, of mutual -> single + params, seems possible. But I didn't try, so the positivity checker may not like it.
Arthur Azevedo de Amorim (Nov 25 2020 at 14:10):Yes, I agree that it would have been possible to encode this away. But the encoding would have been awkward... Moreover, I only had to add the eq instance later on in the development, so I would have had to refactor the code. It is just nice to be able to use inductives without having to think about these issues.
Last updated: Oct 13 2024 at 01:02 UTC