Ali Caglayan (Jul 30 2020 at 17:52): Ali Caglayan (Jul 30 2020 at 17:52):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: Sep 26 2023 at 11:01 UTC