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.
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.
Got it. I'll use something else for now, but I am looking forward to doing the switch to ELPI in the future!
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).
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).
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)
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.
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: Jun 06 2023 at 22:01 UTC