When we define mutual inductive types, we can supply parameters and indices, however coq rejects any attempt to give different parameters. Is there a good reason for this?

This can be observed in the following code:

```
Require Import Prelude.
Inductive fooA : nat -> Type :=
| barA : forall n, fooA n
with fooB : nat -> nat -> Type :=
| barB : forall n m, fooA n -> fooB n m
.
Inductive fooA' (n : nat) : Type :=
| barA' : fooA' n
with fooB' (n : nat) : nat -> Type :=
| barB' : forall m, fooA' n -> fooB' n m
.
Inductive fooA'' (n : nat) : Type :=
| barA'' : fooA'' n
with fooB'' : nat -> nat -> Type :=
| barB'' : forall n m, fooA'' n -> fooB'' n m
.
```

fooA has the most general eliminators, but they could be too powerful for something I want to do. fooA' is the weaker version where both inductives have a parameter. But if I wanted only the weak eliminator for fooA' I cannot give different parameters as I did for fooA''. When I try this I get the message `Parameters should be syntactically the same for each inductive type.`

.

Having the same parameters in every body of the mutual definition seems unnecessarily restrictive to me.

Last updated: Apr 14 2024 at 09:39 UTC