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: Jan 27 2023 at 01:03 UTC