feat : derive DecidableEq for mutual inductives

[arthur-adjedj]

• Put an X in this bracket to confirm you have read the
  External Contribution Guidelines.

This partly implements #2329 by making the derive handler manage mutual inductive types. The general framework for derive handlers is currently not well-suited to manage nested inductives without resorting to making the derived instances partial, and managing them would require big changes to the framework, and thus, to other handlers as well. Such work/design decisions should be discussed in a subsequent RFC.

[github-actions]

Thanks for your contribution! Please make sure to follow our Commit Convention.

[arthur-adjedj]

awaiting-review

[leanprover-community-mathlib4-bot]

• ✅ Mathlib branch lean-pr-testing-2591 has successfully built against this PR. (2023-09-26 18:26:36) View Log
• 🟡 Mathlib branch lean-pr-testing-2591 build against this PR was cancelled. (2023-09-27 08:50:31) View Log
• ❌ Mathlib branch lean-pr-testing-2591 built against this PR, but testing failed. (2023-09-27 09:58:04) View Log
• ❌ Mathlib branch lean-pr-testing-2591 built against this PR, but testing failed. (2023-10-02 11:14:29) View Log
• ✅ Mathlib branch lean-pr-testing-2591 has successfully built against this PR. (2023-10-02 13:15:23) View Log

[semorrison]

I was slightly surprised to find that writing deriving DecidableEq on both inductives in a mutual block didn't error. That's great, but could you explain to me why? :-)

[semorrison]

Would you mind adding a sentence about this to RELEASES.md in the v4.3.0 section (you will need to rebase on master for this section to appear)? We're trying to get better about recording the lovely new features arriving in Lean!

[arthur-adjedj]

I was slightly surprised to find that writing deriving DecidableEq on both inductives in a mutual block didn't error. That's great, but could you explain to me why? :-)

I was surprised by this behaviour too ! As it turns out, other handlers share the same behaviour, so I figured I shouldn't change it here. Another thing that surprised me is that deriving on one inductive doesn't lead to the other one(s) also getting the instances generated. Furthermore, you can't use deriving _ on a whole mutual block, despite handlers being handled arrays of names instead of just a single one. Because of this, you need to derive on each and every inductive, which leads to code duplication of the definitions behind the instances (!). I believe such fixes/changes could (should ?) come through reworking the whole framework as well, instead of it being on a case-by-case basis.